src/HOL/Tools/datatype_realizer.ML
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Sun, 16 Nov 2008 20:03:42 +0100 wenzelm clarified Thm.proof_body_of vs. Thm.proof_of;
Sat, 15 Nov 2008 21:31:17 +0100 wenzelm Thm.proof_of returns proof_body;
Sat, 12 Apr 2008 17:00:35 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Sat, 29 Mar 2008 19:14:03 +0100 wenzelm simplified PureThy.store_thm;
Thu, 20 Mar 2008 12:09:20 +0100 haftmann more antiquotations
Mon, 29 Oct 2007 16:13:41 +0100 wenzelm qualified Proofterm.proofs;
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Tue, 25 Sep 2007 15:34:35 +0200 wenzelm simplified interpretation setup;
Tue, 25 Sep 2007 12:16:08 +0200 haftmann datatype interpretators for size and datatype_realizer
Thu, 05 Jul 2007 20:01:26 +0200 wenzelm renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
Thu, 05 Jul 2007 00:06:14 +0200 wenzelm avoid polymorphic equality;
Sun, 15 Apr 2007 14:31:47 +0200 wenzelm Thm.fold_terms;
Wed, 04 Apr 2007 23:29:33 +0200 wenzelm rep_thm/cterm/ctyp: removed obsolete sign field;
Wed, 04 Apr 2007 00:11:03 +0200 wenzelm removed obsolete sign_of/sign_of_thm;
Tue, 05 Dec 2006 00:30:38 +0100 wenzelm thm/prf: separate official name vs. additional tags;
Wed, 02 Aug 2006 22:26:37 +0200 wenzelm removed obsolete Drule.frees/vars_of etc.;
Tue, 11 Jul 2006 12:16:54 +0200 wenzelm replaced Term.variant(list) by Name.variant(_list);
Wed, 07 Jun 2006 02:01:28 +0200 wenzelm renamed Type.(un)varifyT to Logic.(un)varifyT;
Mon, 06 Feb 2006 20:58:54 +0100 wenzelm Envir.(beta_)eta_contract;
Tue, 06 Dec 2005 09:04:09 +0100 haftmann re-oriented some result tuples in PureThy
Fri, 21 Oct 2005 18:14:38 +0200 wenzelm OldGoals;
Tue, 20 Sep 2005 16:17:34 +0200 haftmann introduced AList module in favor of assoc etc.
Tue, 31 May 2005 11:53:14 +0200 wenzelm Theory.restore_naming;
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.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Tue, 26 Oct 2004 16:25:41 +0200 berghofe Fixed problem with sorts in function make_casedists.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Wed, 27 Nov 2002 17:06:47 +0100 berghofe Changed format of realizers / correctness proofs.
Wed, 13 Nov 2002 15:28:41 +0100 berghofe prove_goal' -> Goal.simple_prove_goal_cterm
Mon, 21 Oct 2002 16:57:39 +0200 berghofe Changed type of Logic.strip_horn.
Thu, 10 Oct 2002 14:26:50 +0200 berghofe Reimplemented parts of datatype package dealing with datatypes involving
Wed, 07 Aug 2002 16:46:15 +0200 berghofe Module for defining realizers for induction and case analysis theorems
less more (0) tip