src/HOL/Tools/datatype_abs_proofs.ML
Tue, 18 Nov 2008 18:25:42 +0100 wenzelm eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
Tue, 07 Oct 2008 16:07:50 +0200 haftmann arbitrary is undefined
Thu, 25 Sep 2008 20:34:15 +0200 wenzelm explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;
Wed, 03 Sep 2008 17:47:30 +0200 wenzelm Sign.declare_const: Name.binding;
Tue, 02 Sep 2008 16:55:33 +0200 wenzelm type Attrib.binding abbreviates Name.binding without attributes;
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Tue, 29 Jul 2008 08:15:40 +0200 haftmann PureThy: dropped note_thmss_qualified, dropped _i suffix
Thu, 17 Apr 2008 22:22:21 +0200 wenzelm prove_global: pass context;
Thu, 03 Apr 2008 17:49:39 +0200 berghofe - use SkipProof.prove_global instead of Goal.prove_global
Sat, 29 Mar 2008 13:03:05 +0100 wenzelm eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
Mon, 25 Feb 2008 16:31:15 +0100 wenzelm inductive package: simplified group handling;
Sat, 26 Jan 2008 17:08:35 +0100 wenzelm internal inductive: fresh theorem group;
Thu, 11 Oct 2007 16:05:23 +0200 wenzelm replaced Sign.add_consts_authentic by Sign.declare_const;
Tue, 02 Oct 2007 22:23:24 +0200 wenzelm inductive: mark internal theorems as Thm.internalK;
Sun, 30 Sep 2007 16:20:31 +0200 wenzelm Sign.add_consts_authentic: tags (Markup.property list);
Fri, 28 Sep 2007 10:32:38 +0200 berghofe Adapted to changes in interface of add_inductive_i.
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Tue, 25 Sep 2007 12:16:08 +0200 haftmann datatype interpretators for size and datatype_realizer
Sat, 15 Sep 2007 19:27:44 +0200 haftmann clarified class interfaces and internals
Fri, 24 Aug 2007 14:14:20 +0200 haftmann overloaded definitions accompanied by explicit constants
Mon, 20 Aug 2007 18:07:30 +0200 haftmann using canonical instantiation interface
Fri, 10 Aug 2007 17:04:24 +0200 haftmann ClassPackage renamed to Class
Thu, 05 Jul 2007 20:01:26 +0200 wenzelm renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
Thu, 17 May 2007 19:49:17 +0200 haftmann abstract size function in hologic.ML
Tue, 24 Apr 2007 15:07:27 +0200 berghofe case constants are now authentic.
Wed, 04 Apr 2007 00:11:03 +0200 wenzelm removed obsolete sign_of/sign_of_thm;
Fri, 01 Dec 2006 17:22:31 +0100 haftmann slight cleanup in hologic.ML
Sun, 26 Nov 2006 18:07:19 +0100 wenzelm InductivePackage.add_inductive_global;
Sat, 18 Nov 2006 00:20:28 +0100 haftmann added instance for class size
Tue, 14 Nov 2006 22:16:55 +0100 wenzelm InductivePackage.add_inductive_i: canonical argument order;
Fri, 10 Nov 2006 22:18:51 +0100 wenzelm simplified LocalTheory.exit;
Fri, 13 Oct 2006 18:18:58 +0200 berghofe Adapted to new inductive definition package.
Tue, 11 Jul 2006 12:16:54 +0200 wenzelm replaced Term.variant(list) by Name.variant(_list);
Sat, 08 Jul 2006 12:54:33 +0200 wenzelm Goal.prove_global;
Fri, 10 Mar 2006 15:33:48 +0100 haftmann renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
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
Thu, 01 Dec 2005 08:28:02 +0100 haftmann oriented pairs theory * 'a to 'a * theory
Tue, 25 Oct 2005 18:18:49 +0200 wenzelm avoid legacy goals;
Fri, 21 Oct 2005 18:14:38 +0200 wenzelm OldGoals;
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Mon, 05 Sep 2005 17:38:18 +0200 wenzelm curried_lookup/update;
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Mon, 24 Jan 2005 18:09:29 +0100 berghofe Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Fri, 21 May 2004 21:48:03 +0200 berghofe Added more flexible parse / print translations for case expressions.
Thu, 10 Oct 2002 14:26:50 +0200 berghofe Reimplemented parts of datatype package dealing with datatypes involving
Wed, 20 Feb 2002 17:30:46 +0100 berghofe Removed superfluous lookup of theorems in Relation.thy
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Wed, 14 Nov 2001 18:44:27 +0100 wenzelm inductive: removed con_defs;
Sat, 27 Oct 2001 00:05:14 +0200 wenzelm hardwire qualified const names;
Sun, 14 Oct 2001 20:04:05 +0200 wenzelm ObjectLogic.atomize_tac;
Fri, 28 Sep 2001 19:19:26 +0200 wenzelm inductive: no collective atts;
Fri, 31 Aug 2001 18:46:48 +0200 wenzelm tuned headers;
Fri, 20 Jul 2001 21:59:11 +0200 wenzelm replaced "Eps" by "The";
Tue, 16 Jan 2001 00:33:40 +0100 wenzelm proper induction rule for arbitrarily branching datatype;
Fri, 13 Oct 2000 08:28:21 +0200 nipkow *** empty log message ***
Thu, 12 Oct 2000 18:38:23 +0200 nipkow *** empty log message ***
less more (0) -60 tip