isabelle: Changelog

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

lcp [Tue, 25 Jul 1995 16:59:08 +0200] rev 1188

Added Part_Int and Part_Collect for inductive definitions

lcp [Tue, 25 Jul 1995 16:58:06 +0200] rev 1187

Includes Sum.thy as a parent for mutual recursion

lcp [Tue, 25 Jul 1995 16:52:08 +0200] rev 1186

now uses proof209.sty

lcp [Tue, 25 Jul 1995 16:50:48 +0200] rev 1185

trivial update

lcp [Tue, 25 Jul 1995 16:43:55 +0200] rev 1184

trivial update

lcp [Tue, 25 Jul 1995 16:34:22 +0200] rev 1183

finally deleted

isabelle