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
where
THEN
OF
Consider rule subst:
$\quad [|\ ?s = ?t; ?P ?s\ |]\quad \Longrightarrow\quad ?P ?t$
Note that you can use this rule only to substitute from left to right, not the reverse. Using OF together with theorem sym ($?s = ?t\ \Longrightarrow\ ?t = ?s$), i.e.
subst [OF sym]
yields
$\quad [|\ ?t = ?s; ?P ?s\ |]\quad \Longrightarrow\quad ?P ?t$
which allows substitutions from right to left.
simplified
rotated
symmetric
reference/attribute_examples.1309948588.txt.gz · Last modified: by 131.246.161.187