urbanc [Mon, 07 Nov 2005 14:35:25 +0100] rev 18104
added thms perm, distinct and fresh to the simplifier.
One would liket to add also inject, but this causes
problems with "congruences" like
Lam [a].t1 = Lam [b].t2
P (Lam [a].t1)
-----------------------
P (Lam [b].t2)
because the equation "Lam [a].t1 = Lam [b].t2" would simplify
to "[a].t1 = [b].t2" and then the goal is not true just by
simplification.
haftmann [Mon, 07 Nov 2005 12:06:11 +0100] rev 18103
added proper fillin_mixfix
haftmann [Mon, 07 Nov 2005 11:39:24 +0100] rev 18102
added fillin_mixfix, replace_quote
berghofe [Mon, 07 Nov 2005 11:28:34 +0100] rev 18101
New function store_thmss_atts.
urbanc [Mon, 07 Nov 2005 11:17:45 +0100] rev 18100
used the function Library.product for the cprod from Stefan
urbanc [Mon, 07 Nov 2005 10:47:25 +0100] rev 18099
fixed bug with nominal induct
- the bug occured in rule inductions when
the goal did not use all variables from
the relation over which the induction
was done
haftmann [Mon, 07 Nov 2005 09:34:51 +0100] rev 18098
added fillin_mixfix' needed by serializer