src/HOL/Tools/typedef_package.ML
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Wed, 31 Dec 2008 00:08:11 +0100 wenzelm use regular Term.add_vars, Term.add_frees etc.;
Thu, 11 Dec 2008 16:30:35 +0100 wenzelm recovered goal_pat;
Thu, 11 Dec 2008 16:09:12 +0100 wenzelm inhabitance goal is now stated in original form and result contracted --
Thu, 11 Dec 2008 11:55:46 +0100 wenzelm add_typedef: unfold set_def in tactical proof as well;
Thu, 11 Dec 2008 10:41:37 +0100 wenzelm Theory.checkpoint before commencing proof;
Thu, 11 Dec 2008 00:42:52 +0100 wenzelm misc tuning and modernisation;
Mon, 08 Dec 2008 08:56:30 +0100 krauss logically separate typedef axiomatization from constant definition
Mon, 08 Dec 2008 08:36:16 +0100 krauss add def before setting up goal
Sun, 07 Dec 2008 20:41:23 +0100 krauss killed dead code
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Wed, 19 Nov 2008 08:58:57 +0100 haftmann explicit inhabitance proof
Wed, 22 Oct 2008 14:15:44 +0200 haftmann tuned typedef interface
Tue, 29 Jul 2008 08:15:40 +0200 haftmann PureThy: dropped note_thmss_qualified, dropped _i suffix
Wed, 25 Jun 2008 17:38:32 +0200 wenzelm moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sat, 29 Mar 2008 13:03:09 +0100 wenzelm eliminated quiete_mode ref (not really needed);
Wed, 05 Dec 2007 14:15:48 +0100 haftmann interpretation of typedefs
Fri, 30 Nov 2007 20:13:07 +0100 haftmann interpretation for typedefs
Wed, 28 Nov 2007 16:44:20 +0100 wenzelm ObjectLogic.typedecl;
Fri, 23 Nov 2007 21:09:30 +0100 haftmann separated typedecl module, providing typedecl command with interpretation
Tue, 09 Oct 2007 17:10:34 +0200 wenzelm AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Sat, 06 Oct 2007 16:50:04 +0200 wenzelm simplified interfaces for outer syntax;
Fri, 05 Oct 2007 22:00:15 +0200 wenzelm tuned Induct interface: prefer pred'' over set'';
Thu, 04 Oct 2007 14:42:47 +0200 wenzelm moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Sat, 01 Sep 2007 15:47:01 +0200 wenzelm replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
Tue, 14 Aug 2007 13:20:12 +0200 wenzelm PrimitiveDefs.mk_defpair;
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Tue, 28 Nov 2006 00:35:18 +0100 wenzelm simplified '?' operator;
Tue, 21 Nov 2006 18:07:30 +0100 wenzelm simplified Proof.theorem(_i);
Tue, 14 Nov 2006 15:29:52 +0100 wenzelm simplified Proof.theorem(_i) interface;
Tue, 14 Nov 2006 00:15:42 +0100 wenzelm removed legacy read/cert/string_of;
Wed, 06 Sep 2006 10:01:04 +0200 haftmann TypedefPackage.add_typedef_* now yields name of introduced type constructor
Fri, 01 Sep 2006 23:18:01 +0200 wenzelm signature: do not export private stuff;
Tue, 08 Aug 2006 08:20:24 +0200 haftmann fixed code generator theorem generation
Sat, 08 Jul 2006 12:54:33 +0200 wenzelm Goal.prove_global;
Wed, 24 May 2006 01:04:57 +0200 wenzelm simplified info/get_info;
Thu, 11 May 2006 19:19:31 +0200 wenzelm avoid raw equality on type thm;
Sun, 07 May 2006 00:22:05 +0200 wenzelm removed 'concl is' patterns;
Sun, 30 Apr 2006 22:50:03 +0200 wenzelm AxClass.axiomatize_arity_i;
Wed, 26 Apr 2006 22:38:05 +0200 wenzelm tuned;
Mon, 24 Apr 2006 16:37:52 +0200 haftmann seperated typedef codegen from main code
Mon, 10 Apr 2006 00:33:49 +0200 wenzelm Term.itselfT;
Thu, 06 Apr 2006 16:09:20 +0200 haftmann added functions for definitional code generation
Tue, 07 Feb 2006 19:56:45 +0100 wenzelm renamed gen_duplicates to duplicates;
Mon, 06 Feb 2006 11:01:28 +0100 haftmann subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
Fri, 27 Jan 2006 19:03:02 +0100 wenzelm moved theorem tags from Drule to PureThy;
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Sat, 14 Jan 2006 17:14:06 +0100 wenzelm sane ERROR handling;
Tue, 10 Jan 2006 19:34:04 +0100 wenzelm generic attributes;
Fri, 09 Dec 2005 09:06:45 +0100 haftmann oriented result pairs in PureThy
Tue, 06 Dec 2005 09:04:09 +0100 haftmann re-oriented some result tuples in PureThy
Fri, 21 Oct 2005 18:14:34 +0200 wenzelm Goal.prove;
Wed, 19 Oct 2005 21:52:34 +0200 wenzelm removed obsolete add_typedef_x;
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Tue, 13 Sep 2005 22:19:23 +0200 wenzelm tuned Isar interfaces;
Tue, 06 Sep 2005 16:59:55 +0200 wenzelm proper treatment of polymorphic sets;
less more (0) -100 -60 tip