src/HOL/indrule.ML
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
1996-07-16 paulson 1996-07-16 corrected comment
1996-07-15 paulson 1996-07-15 Uses minimal simpset (min_ss) and full_simp_tac instead of asm_full_simp_tac to prevent excessive simplification, which can cause proofs to fail
1996-05-17 nipkow 1996-05-17 Moved split_rule et al from ind_syntax.ML to Prod.ML. Used split_rule in Lfp.ML and Trancl.ML.
1996-05-07 paulson 1996-05-07 Unfolding of arbitrarily nested tuples in induction rules
1996-04-04 nipkow 1996-04-04 Replaced !simpset by HOL_ss on line 93.
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-12-28 paulson 1995-12-28 Now mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-07-25 lcp 1995-07-25 Old version of mutual induction never worked. Now ensures that all predicates get the SAME type. Updated mutual_ind_tac from ZF version
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application