src/HOL/Tools/primrec_package.ML
Sat, 30 May 2009 08:17:05 +0200 haftmann simps with mandatory name prefix
Wed, 27 May 2009 22:11:06 +0200 haftmann tuned signature of add_primrec_simple
Tue, 26 May 2009 17:29:34 +0200 haftmann add_primrec_simple
Mon, 18 May 2009 09:48:06 +0200 haftmann introduced Thm.generatedK
Sat, 16 May 2009 20:17:59 +0200 bulwahn added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
Sat, 16 May 2009 15:23:52 +0200 bulwahn added collection of simplification rules of recursive functions for quickcheck
Thu, 12 Mar 2009 21:55:02 +0100 wenzelm simplified preparation and outer parsing of specification;
Wed, 11 Mar 2009 19:27:48 +0100 wenzelm merged
Wed, 11 Mar 2009 15:56:52 +0100 haftmann corrected type inference of primitive definitions
Wed, 11 Mar 2009 15:42:19 +0100 wenzelm explicit Binding.qualified_name -- prevents implicitly qualified bstring;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Thu, 05 Mar 2009 12:08:00 +0100 wenzelm renamed NameSpace.base to NameSpace.base_name;
Tue, 03 Mar 2009 18:32:01 +0100 wenzelm renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
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;
less more (0) -100 -60 tip