src/HOL/Tools/primrec_package.ML
Mon, 09 Feb 2009 10:37:59 +0100 blanchet Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
Fri, 06 Feb 2009 15:59:49 +0100 blanchet Merged.
Fri, 06 Feb 2009 15:57:47 +0100 blanchet Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
Thu, 05 Feb 2009 14:14:03 +0100 haftmann code attribute applied before user attributes
Wed, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Wed, 31 Dec 2008 19:54:03 +0100 wenzelm qualified Term.rename_wrt_term;
Wed, 31 Dec 2008 00:08:13 +0100 wenzelm moved old add_term_vars, add_term_frees etc. to structure OldTerm;
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, 07 Oct 2008 16:07:30 +0200 haftmann proper default codegen attribute
Mon, 29 Sep 2008 10:58:01 +0200 wenzelm LocalTheory.exit_global;
Wed, 03 Sep 2008 11:44:48 +0200 wenzelm Name.qualified;
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;
Fri, 20 Jun 2008 21:00:25 +0200 haftmann fixed bind error for malformed primrec specifications
Wed, 16 Apr 2008 10:57:46 +0200 berghofe Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).
Fri, 04 Apr 2008 13:40:23 +0200 haftmann prefix for equations in primrec specifications
Mon, 25 Feb 2008 16:31:17 +0100 wenzelm LocalTheory.set_group for user command;
Tue, 11 Dec 2007 10:23:11 +0100 haftmann dropped induction rule
Fri, 07 Dec 2007 15:07:56 +0100 haftmann proper treatment of code theorems for primrec
Fri, 07 Dec 2007 08:38:50 +0100 haftmann tuned further
Thu, 06 Dec 2007 16:56:00 +0100 haftmann fixed slip
Thu, 06 Dec 2007 16:36:19 +0100 haftmann authentic primrec
Thu, 06 Dec 2007 15:10:09 +0100 haftmann added new primrec package
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, 25 Sep 2007 13:28:37 +0200 wenzelm Syntax.parse/check/read;
Tue, 18 Sep 2007 07:36:15 +0200 haftmann distinction between regular and default code theorems
Thu, 30 Aug 2007 22:35:34 +0200 wenzelm replaced ProofContext.infer_types by general Syntax.check_terms;
Wed, 11 Jul 2007 11:44:51 +0200 berghofe Function unify_consts moved from OldInductivePackage to PrimrecPackage.
Wed, 18 Apr 2007 21:30:14 +0200 wenzelm simplified ProofContext.infer_types(_pats);
Sun, 15 Apr 2007 14:31:49 +0200 wenzelm proper ProofContext.infer_types;
Tue, 20 Mar 2007 15:52:37 +0100 haftmann switched exception from arbitrary to undefined
Fri, 19 Jan 2007 22:08:08 +0100 wenzelm moved parts of OuterParse to SpecParse;
Fri, 20 Oct 2006 10:44:47 +0200 haftmann fold cleanup
Fri, 13 Oct 2006 18:23:37 +0200 berghofe Moved old inductive package to old_inductive_package.ML
Mon, 02 Oct 2006 23:01:00 +0200 haftmann added gen_primrec
Fri, 21 Jul 2006 14:46:27 +0200 haftmann exported equation transformator
Sat, 08 Jul 2006 12:54:33 +0200 wenzelm Goal.prove_global;
Sat, 20 May 2006 23:36:57 +0200 wenzelm added syntax for 'unchecked';
Sat, 13 May 2006 02:51:49 +0200 wenzelm added add_primrec_unchecked_i;
Wed, 15 Feb 2006 21:34:55 +0100 wenzelm removed distinct, renamed gen_distinct to distinct;
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
Sat, 21 Jan 2006 23:02:14 +0100 wenzelm simplified type attribute;
Sat, 14 Jan 2006 22:25:34 +0100 wenzelm generic attributes;
Sat, 14 Jan 2006 17:14:06 +0100 wenzelm sane ERROR handling;
Fri, 09 Dec 2005 09:06:45 +0100 haftmann oriented result pairs in PureThy
Tue, 06 Dec 2005 17:26:26 +0100 haftmann removed thms 'swap' and 'nth_map' from ML toplevel
Tue, 06 Dec 2005 09:04:09 +0100 haftmann re-oriented some result tuples in PureThy
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;
Thu, 08 Sep 2005 16:09:23 +0200 haftmann introduces some modern-style AList operations
Mon, 05 Sep 2005 17:38:18 +0200 wenzelm curried_lookup/update;
Mon, 29 Aug 2005 16:18:04 +0200 wenzelm use AList operations;
Tue, 16 Aug 2005 13:42:26 +0200 wenzelm OuterKeyword;
Fri, 08 Jul 2005 11:57:15 +0200 berghofe Some changes to allow mutually recursive, overloaded functions with same name.
Fri, 01 Jul 2005 14:14:40 +0200 berghofe Adapted to new interface of RecfunCodegen.add.
less more (0) -100 -60 tip