src/ZF/Tools/inductive_package.ML
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Replaced xstring by thmref.
2002-12-12 paulson 2002-12-12 Better treatment of equality in premises of inductive definitions. Less backtracking.
2002-10-04 paulson 2002-10-04 Fixed bug involving inductive definitions with equalities in the premises.
2002-02-20 wenzelm 2002-02-20 Symbol.bump_string;
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2002-01-12 wenzelm 2002-01-12 renamed forall_elim_vars_safe to gen_all;
2002-01-11 wenzelm 2002-01-11 replace gen_all by forall_elim_vars_safe;
2001-11-19 wenzelm 2001-11-19 tuned;
2001-11-16 wenzelm 2001-11-16 actually store "coinduct" rule;
2001-11-14 wenzelm 2001-11-14 case_names;
2001-11-14 wenzelm 2001-11-14 adapted primrec/datatype to Isar;
2001-11-13 wenzelm 2001-11-13 rearranged inductive package for Isar;
2001-11-09 wenzelm 2001-11-09 support co/inductive definitions in new-style theories;
2001-10-04 wenzelm 2001-10-04 qualify MetaSimplifier;
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-05-05 wenzelm 2000-05-05 use Sign.simple_read_term;
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
1999-10-04 wenzelm 1999-10-04 mk_frees, assume_read moved here; FOLogic.mk_conj, FOLogic.mk_disj;
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-02-03 paulson 1999-02-03 standard spelling: type-checking
1999-01-19 paulson 1999-01-19 removal of the (thm list) argument of mk_cases
1999-01-12 wenzelm 1999-01-12 eliminated global/local names;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-12-28 paulson 1998-12-28 revised inductive definition package