src/HOL/Inductive.ML
1997-04-02 paulson 1997-04-02 Now calls require_thy to ensure ancestors are present
1996-01-30 clasohm 1996-01-30 expanded tabs
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