Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-02-02 15:16:21 -0800 (Fri, 02 Feb 2001)
Revision: 3137
Log message:
The itt_squiggle theory is added at last.
Now a ~ b is a type as well as any other type.
To substitute 'a for 'b in nth clause you can use
sqSubstT <<a ~ b>> n
or you can use Itt_subst2.substT tactic instead. (Note that
Itt_subst.substT works only with an equality).
The sqSubst tactic works exactly as the substT tactic.
By default it replaces all occurrences of a with b, or
one can give a bind term as an optional with-argument to specify
the occurrences of a to be replaced.
Example 1:
H |- a+a=2*a
by substT <<'a ~ 'b>> 0
1. ....rewrite....
H |- a <--> b
2. ....main....
H |- b+b=2*b
Example 2:
H |- a+a=2*a
by withT <<bind{x.'x+'x=2*'a}>> (substT <<'a ~ 'b>> 0)
1. ....rewrite....
H |- a <--> b
2. ....main....
H |- b+b=2*a
I'll document this theory later.
Still to do: Figure out how to make conversion "a -> b" from "a~b".
P.S. You probably need to run make clean in theories/itt before recompiling.