1995-07-25 agoAdded weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp [Tue, 25 Jul 1995 17:03:16 +0200] rev 1194
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)

1995-07-25 agoCorrected mixfix declaration of @perm
lcp [Tue, 25 Jul 1995 17:02:34 +0200] rev 1193
Corrected mixfix declaration of @perm

1995-07-25 agoProved perm_length
lcp [Tue, 25 Jul 1995 17:02:03 +0200] rev 1192
Proved perm_length

1995-07-25 agoAdded two final lines to intro_tacsf for mutual recursion
lcp [Tue, 25 Jul 1995 17:01:25 +0200] rev 1191
Added two final lines to intro_tacsf for mutual recursion
(borrowed from ZF version)

1995-07-25 agoOld version of mutual induction never worked. Now ensures that
lcp [Tue, 25 Jul 1995 17:00:53 +0200] rev 1190
Old version of mutual induction never worked. Now ensures that
all predicates get the SAME type. Updated mutual_ind_tac from ZF version

1995-07-25 agoChanged comments
lcp [Tue, 25 Jul 1995 17:00:15 +0200] rev 1189
Changed comments

1995-07-25 agoAdded Part_Int and Part_Collect for inductive definitions
lcp [Tue, 25 Jul 1995 16:59:08 +0200] rev 1188
Added Part_Int and Part_Collect for inductive definitions

1995-07-25 agoIncludes Sum.thy as a parent for mutual recursion
lcp [Tue, 25 Jul 1995 16:58:06 +0200] rev 1187
Includes Sum.thy as a parent for mutual recursion

1995-07-25 agonow uses proof209.sty
lcp [Tue, 25 Jul 1995 16:52:08 +0200] rev 1186
now uses proof209.sty

1995-07-25 agotrivial update
lcp [Tue, 25 Jul 1995 16:50:48 +0200] rev 1185
trivial update