src/HOL/Tools/typedef_package.ML
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
2000-01-25 wenzelm 2000-01-25 fallback on PureThy version;
2000-01-05 wenzelm 2000-01-05 replaced HOLogic.termTVar by HOLogic.termT;
1999-09-04 wenzelm 1999-09-04 goal_nonempty: Ex goal for new-style version;
1999-08-02 wenzelm 1999-08-02 tuned outer syntax;
1999-07-08 wenzelm 1999-07-08 propp: 'concl' patterns;
1999-05-25 wenzelm 1999-05-25 formal comments (still dummy);
1999-05-24 wenzelm 1999-05-24 outer syntax keyword classification; no open OuterParse;
1999-05-21 wenzelm 1999-05-21 typedef_proof: pass interactive flag;
1999-03-17 wenzelm 1999-03-17 actually check non-emptiness theorem; added typedef_proof(_i); 'typedef' outer syntax;
1999-03-11 wenzelm 1999-03-11 named witnesses: PureThy.get_thmss; outer syntax for 'typedecl', 'typedef';
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-10-20 wenzelm 1998-10-20 quiet_mode, message;
1998-07-24 berghofe 1998-07-24 Added new function add_typedef_i_no_def which doesn't add definition of representing set to theory.
1998-07-01 wenzelm 1998-07-01 added add_typedecls;
1998-05-27 paulson 1998-05-27 Changed require to requires for MLWorks
1998-05-15 wenzelm 1998-05-15 PureThy.add_typedecls;
1998-04-29 wenzelm 1998-04-29 renamed from typedef.ML;