isabelle: Changelog

lcp [Tue, 25 Jul 1995 17:03:59 +0200] rev 1195

match_bvs no longer puts a name in the alist if it is null ("")

lcp [Tue, 25 Jul 1995 17:03:16 +0200] rev 1194

Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)

lcp [Tue, 25 Jul 1995 17:02:34 +0200] rev 1193

Corrected mixfix declaration of @perm

lcp [Tue, 25 Jul 1995 17:02:03 +0200] rev 1192

Proved perm_length

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)

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

lcp [Tue, 25 Jul 1995 17:00:15 +0200] rev 1189

Changed comments

isabelle