src/HOL/add_ind_def.ML
1997-11-17 wenzelm 1997-11-17 improved big_rec_name lookup;
1997-10-28 wenzelm 1997-10-28 PureThy.add_store_defs_i;
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1997-10-01 wenzelm 1997-10-01 fully qualified names: Theory.add_XXX;
1997-04-21 paulson 1997-04-21 Disabled the attempts for mutual induction to work so that single induction involving sum types can work
1997-04-02 paulson 1997-04-02 Now tests for essential ancestors (Lfp or Gfp)
1996-11-28 paulson 1996-11-28 Replaced map...~~ by ListPair.map
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-12-08 paulson 1995-12-08 Improved error message, suggesting addition of type constraints if occurrences of the recursive set remain in the fixedpoint definition.
1995-07-25 lcp 1995-07-25 Changed comments
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application