src/HOL/Tools/recdef_package.ML
Tue, 10 Feb 2009 14:58:15 +0100 blanchet Added nitpick_const_simp attribute to recdef and record packages.
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Fri, 05 Dec 2008 18:43:42 +0100 haftmann Name.name_of -> Binding.base_name
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Tue, 28 Oct 2008 16:58:59 +0100 haftmann cleanup code default attribute
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;
Sat, 09 Aug 2008 22:43:46 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Mon, 04 Aug 2008 20:27:37 +0200 wenzelm simplified defer_recdef(_i): plain facts via Attrib.eval_thms;
Wed, 25 Jun 2008 17:38:32 +0200 wenzelm moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
Sat, 24 May 2008 22:04:52 +0200 wenzelm more uniform treatment of OuterSyntax.local_theory commands;
Sat, 29 Mar 2008 13:03:09 +0100 wenzelm eliminated quiete_mode ref (not really needed);
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Tue, 09 Oct 2007 17:10:36 +0200 wenzelm Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
Sat, 06 Oct 2007 16:50:04 +0200 wenzelm simplified interfaces for outer syntax;
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Tue, 18 Sep 2007 07:36:15 +0200 haftmann distinction between regular and default code theorems
Tue, 28 Aug 2007 18:14:17 +0200 berghofe Adapted to changes in interface of Specification.theorem_i
Sun, 29 Jul 2007 14:29:54 +0200 wenzelm renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Mon, 26 Feb 2007 23:18:24 +0100 wenzelm moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
Fri, 19 Jan 2007 22:08:08 +0100 wenzelm moved parts of OuterParse to SpecParse;
Thu, 23 Nov 2006 22:38:29 +0100 wenzelm prefer Proof.context over Context.generic;
Tue, 21 Nov 2006 18:07:30 +0100 wenzelm simplified Proof.theorem(_i);
Tue, 14 Nov 2006 00:15:39 +0100 wenzelm recdef_tc(_i): local_theory interface via Specification.theorem_i;
Mon, 23 Oct 2006 16:49:21 +0200 haftmann switched merge_alists'' to AList.merge'' whenever appropriate
Fri, 20 Oct 2006 17:07:26 +0200 haftmann slight cleanup
Wed, 02 Aug 2006 22:26:45 +0200 wenzelm export get_hints;
Mon, 05 Jun 2006 14:26:07 +0200 krauss HOL/Tools/function_package: Added support for mutual recursive definitions.
Sat, 20 May 2006 23:36:55 +0200 wenzelm List.partition;
Sun, 07 May 2006 00:22:05 +0200 wenzelm removed 'concl is' patterns;
Fri, 05 May 2006 17:17:21 +0200 krauss First usable version of the new function definition package (HOL/function_packake/...).
Thu, 02 Feb 2006 10:24:06 +0100 krauss Exporting recdef's hints for use by new recdef package
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 22:25:34 +0100 wenzelm generic attributes;
Fri, 16 Dec 2005 09:00:11 +0100 haftmann re-arranged tuples (theory * 'a) to ('a * theory) in Pure
Fri, 09 Dec 2005 09:06:45 +0100 haftmann oriented result pairs in PureThy
Wed, 19 Oct 2005 21:52:32 +0200 wenzelm removed obsolete add_recdef_old;
Fri, 23 Sep 2005 09:00:19 +0200 haftmann temporarily re-introduced overwrite_warn
Wed, 21 Sep 2005 17:25:32 +0200 haftmann introduces update_warn instead of overwrite_warn
Tue, 20 Sep 2005 08:21:49 +0200 haftmann slight adaptions to library changes
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Tue, 13 Sep 2005 22:19:19 +0200 wenzelm tuned IsarThy.theorem_i;
Mon, 05 Sep 2005 17:38:18 +0200 wenzelm curried_lookup/update;
Tue, 16 Aug 2005 13:42:26 +0200 wenzelm OuterKeyword;
Fri, 01 Jul 2005 14:14:40 +0200 berghofe Adapted to new interface of RecfunCodegen.add.
Fri, 17 Jun 2005 18:35:27 +0200 wenzelm accomodate change of TheoryDataFun;
Sat, 11 Jun 2005 22:15:48 +0200 wenzelm refer to name spaces values instead of names;
Tue, 31 May 2005 11:53:13 +0200 wenzelm renamed cond_extern to extern;
Wed, 13 Apr 2005 18:45:25 +0200 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
Wed, 13 Apr 2005 18:34:22 +0200 wenzelm *** empty log message ***
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.
Mon, 24 Jan 2005 18:07:10 +0100 berghofe Replaced xstring by thmref.
Sun, 11 Jul 2004 20:33:22 +0200 wenzelm local_cla/simpset_of;
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Fri, 17 Oct 2003 11:04:36 +0200 paulson Prevent recdef from looping when the inductio rule is simplified
less more (0) -100 -60 tip