src/HOL/ind_syntax.ML
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-01-30 clasohm 1996-01-30 expanded tabs
1996-01-06 nipkow 1996-01-06 removed reference to Nat thms in elim_rls.
1996-01-02 paulson 1996-01-02 Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule.
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application