User Tools
reference:attribute_examples
This is an old revision of the document!
Table of Contents
Attribute Examples
This page contains usage examples for attributes (or directives).
of
Consider rule/theorem mp:
.
Using
mp [of _ "C ∨ D"]
yields the more specific theorem
.
Note that are no longer schematic variables but specific terms.
where
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.
THEN
OF
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.
simplified
rotated
Consider rule disjE:
.
Then,
disjE [rotated 2]
yields
.
symmetric
reference/attribute_examples.1309949420.txt.gz · Last modified: 2011/07/06 12:50 by 131.246.161.187
