Mon, 07 Nov 2005 15:19:03 +0100 Initial commit.
urbanc [Mon, 07 Nov 2005 15:19:03 +0100] rev 18106
Initial commit.
Mon, 07 Nov 2005 15:12:13 +0100 Initial commit of the theory "Weakening".
urbanc [Mon, 07 Nov 2005 15:12:13 +0100] rev 18105
Initial commit of the theory "Weakening".
Mon, 07 Nov 2005 14:35:25 +0100 added thms perm, distinct and fresh to the simplifier.
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.
Mon, 07 Nov 2005 12:06:11 +0100 added proper fillin_mixfix
haftmann [Mon, 07 Nov 2005 12:06:11 +0100] rev 18103
added proper fillin_mixfix
Mon, 07 Nov 2005 11:39:24 +0100 added fillin_mixfix, replace_quote
haftmann [Mon, 07 Nov 2005 11:39:24 +0100] rev 18102
added fillin_mixfix, replace_quote
Mon, 07 Nov 2005 11:28:34 +0100 New function store_thmss_atts.
berghofe [Mon, 07 Nov 2005 11:28:34 +0100] rev 18101
New function store_thmss_atts.
Mon, 07 Nov 2005 11:17:45 +0100 used the function Library.product for the cprod from Stefan
urbanc [Mon, 07 Nov 2005 11:17:45 +0100] rev 18100
used the function Library.product for the cprod from Stefan
Mon, 07 Nov 2005 10:47:25 +0100 fixed bug with nominal induct
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
Mon, 07 Nov 2005 09:34:51 +0100 added fillin_mixfix' needed by serializer
haftmann [Mon, 07 Nov 2005 09:34:51 +0100] rev 18098
added fillin_mixfix' needed by serializer
Sun, 06 Nov 2005 01:21:37 +0100 add case syntax stuff
huffman [Sun, 06 Nov 2005 01:21:37 +0100] rev 18097
add case syntax stuff
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip