src/ZF/Tools/datatype_package.ML
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-15 wenzelm 2006-01-15 classical attributes: optional weight;
2006-01-14 wenzelm 2006-01-14 generic attributes;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-11-16 wenzelm 2005-11-16 Term.betapplys;
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-19 wenzelm 2005-10-19 removed obsolete add_datatype_x; tuned;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src;
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-05-15 paulson 2002-05-15 better error messages for datatypes not declared Const
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2001-11-19 wenzelm 2001-11-19 tuned;
2001-11-16 wenzelm 2001-11-16 additional P.marg_comment;
2001-11-14 wenzelm 2001-11-14 use proper intr_names (for required case_names); store con_defs, case_eqns, recursor_eqns, free_iffs, free_elims;
2001-11-14 wenzelm 2001-11-14 adapted primrec/datatype to Isar;
2001-11-09 wenzelm 2001-11-09 adapted to add_inductive_x;
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.;
2000-01-13 paulson 2000-01-13 change in add_thmss to suppress warning
1999-10-04 wenzelm 1999-10-04 tuned;
1999-01-27 paulson 1999-01-27 automatic insertion of datatype intr rules into claset
1999-01-19 paulson 1999-01-19 removal of the (thm list) argument of mk_cases
1999-01-13 paulson 1999-01-13 datatype package improvements
1999-01-12 wenzelm 1999-01-12 eliminated global/local names;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1999-01-07 paulson 1999-01-07 ZF: the natural numbers as a datatype
1999-01-06 paulson 1999-01-06 induct_tac and exhaust_tac
1998-12-28 paulson 1998-12-28 revised datatype definition package