src/HOL/Tools/typedef_package.ML
Sat, 01 Jul 2000 19:55:22 +0200 wenzelm GPLed;
Mon, 13 Mar 2000 13:16:57 +0100 wenzelm adapted to new PureThy.add_thms etc.;
Tue, 25 Jan 2000 20:22:57 +0100 wenzelm fallback on PureThy version;
Wed, 05 Jan 2000 11:56:04 +0100 wenzelm replaced HOLogic.termTVar by HOLogic.termT;
Sat, 04 Sep 1999 21:13:55 +0200 wenzelm goal_nonempty: Ex goal for new-style version;
Mon, 02 Aug 1999 17:58:23 +0200 wenzelm tuned outer syntax;
Thu, 08 Jul 1999 18:36:09 +0200 wenzelm propp: 'concl' patterns;
Tue, 25 May 1999 20:24:10 +0200 wenzelm formal comments (still dummy);
Mon, 24 May 1999 21:57:13 +0200 wenzelm outer syntax keyword classification;
Fri, 21 May 1999 11:48:42 +0200 wenzelm typedef_proof: pass interactive flag;
Wed, 17 Mar 1999 13:49:14 +0100 wenzelm actually check non-emptiness theorem;
Thu, 11 Mar 1999 21:57:34 +0100 wenzelm named witnesses: PureThy.get_thmss;
Tue, 12 Jan 1999 13:54:51 +0100 wenzelm eliminated tthm type and Attribute structure;
Tue, 20 Oct 1998 16:37:02 +0200 wenzelm quiet_mode, message;
Fri, 24 Jul 1998 12:55:05 +0200 berghofe Added new function add_typedef_i_no_def which doesn't add
Wed, 01 Jul 1998 11:20:32 +0200 wenzelm added add_typedecls;
Wed, 27 May 1998 12:21:39 +0200 paulson Changed require to requires for MLWorks
Fri, 15 May 1998 11:34:12 +0200 wenzelm PureThy.add_typedecls;
Wed, 29 Apr 1998 11:39:52 +0200 wenzelm renamed from typedef.ML;
less more (0) tip