src/HOL/Tools/typedef_package.ML
2001-10-17 wenzelm 2001-10-17 improved internal interface of typedef;
2001-10-16 wenzelm 2001-10-16 typedef: export result;
2001-10-13 wenzelm 2001-10-13 'morphisms' spec; tuned goal pattern for set;
2001-10-13 wenzelm 2001-10-13 IsarThy.theorem_i Drule.internalK;
2001-10-12 wenzelm 2001-10-12 test: use SkipProof.make_thm instead of Thm.assume;
2001-09-27 wenzelm 2001-09-27 renamed theory "subset" to "Typedef";
2001-07-15 wenzelm 2001-07-15 abtract non-emptiness statements (no longer use Eps); cleaned up;
2000-12-19 wenzelm 2000-12-19 improved errors;
2000-12-14 wenzelm 2000-12-14 'typedef': present result theorem "type_definition Rep Abs A";
2000-12-06 wenzelm 2000-12-06 less rude treatment of "no_def";
2000-11-13 wenzelm 2000-11-13 tuned IsarThy.theorem_i;
2000-10-19 wenzelm 2000-10-19 provide more theorems (see subset.thy); tuned;
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-07-01 wenzelm 2000-07-01 GPLed;
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;