src/HOL/Tools/typedef_package.ML
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;
Mon, 05 Sep 2005 17:38:18 +0200 wenzelm curried_lookup/update;
Thu, 25 Aug 2005 16:10:16 +0200 berghofe Implemented incremental code generation.
Tue, 16 Aug 2005 13:42:26 +0200 wenzelm OuterKeyword;
Fri, 01 Jul 2005 14:13:40 +0200 berghofe Adapted to modular code generation.
Mon, 20 Jun 2005 22:13:59 +0200 wenzelm get_thm(s): Name;
Fri, 17 Jun 2005 18:35:27 +0200 wenzelm accomodate change of TheoryDataFun;
Tue, 31 May 2005 11:53:17 +0200 wenzelm fixed outer syntax: allow type_args with parentheses;
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Mon, 24 Jan 2005 17:59:48 +0100 berghofe Adapted to modified interface of PureThy.get_thm(s).
Wed, 27 Oct 2004 10:30:07 +0200 berghofe Added type constraint to make SML/NJ happy.
Tue, 26 Oct 2004 16:30:32 +0200 berghofe Added simple code generator.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Sat, 29 May 2004 14:58:44 +0200 wenzelm Library.read_int;
Thu, 15 Apr 2004 20:30:50 +0200 wenzelm finalconsts RepC AbsC;
Fri, 02 Aug 2002 11:49:55 +0200 wenzelm typedef: "open" option;
Wed, 24 Jul 2002 00:11:24 +0200 wenzelm adapted fact names;
Tue, 12 Feb 2002 20:28:27 +0100 wenzelm got rid of explicit marginal comments (now stripped earlier from input);
less more (0) -60 tip