Table of Contents

This page contains usage examples for attributes (or directives).

Consider rule/theorem `mp`

:

.

Using

mp [of _ "C ∨ D"]

yields the more specific theorem

.

Note that are no longer schematic variables but specific terms.

Consider rule/theorem `mp`

:

.

Using

mp [where Q="C ∨ D"]

yields the more specific theorem

.

Note that are no longer schematic variables but specific terms.

Consider the “composite” theorem

Then,

t [THEN conjunct1]

yields the new theorem

Consider rule `subst`

:

Note that you can use this rule only to substitute from left to right, not the reverse. Using `OF`

together with theorem `sym`

(), i.e.

subst [OF sym]

yields

which allows substitutions from right to left.

Consider theorem `Nat.le_square`

:

Using

Nat.le_square [simplified]

you get

Wether or not this is actually “simpler” is certainly open to discussion, especially because the original form does say something about while the `simplified`

version does not.

Consider rule `disjE`

:

.

Then,

disjE [rotated 2]

yields

.

Consider the definition of set membership `Set.mem_def`

,

.

Then,

test [symmetric]

yields

.