| Sat, 30 May 2009 08:17:05 +0200 |
simps with mandatory name prefix
|
file | diff | annotate |
| Wed, 27 May 2009 22:11:06 +0200 |
tuned signature of add_primrec_simple
|
file | diff | annotate |
| Tue, 26 May 2009 17:29:34 +0200 |
add_primrec_simple
|
file | diff | annotate |
| Mon, 18 May 2009 09:48:06 +0200 |
introduced Thm.generatedK
|
file | diff | annotate |
| Sat, 16 May 2009 20:17:59 +0200 |
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
|
file | diff | annotate |
| Sat, 16 May 2009 15:23:52 +0200 |
added collection of simplification rules of recursive functions for quickcheck
|
file | diff | annotate |
| Thu, 12 Mar 2009 21:55:02 +0100 |
simplified preparation and outer parsing of specification;
|
file | diff | annotate |
| Wed, 11 Mar 2009 19:27:48 +0100 |
merged
|
file | diff | annotate |
| Wed, 11 Mar 2009 15:42:19 +0100 |
explicit Binding.qualified_name -- prevents implicitly qualified bstring;
|
file | diff | annotate |
| Wed, 11 Mar 2009 15:56:52 +0100 |
corrected type inference of primitive definitions
|
file | diff | annotate |
| Sun, 08 Mar 2009 17:26:14 +0100 |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file | diff | annotate |
| Thu, 05 Mar 2009 12:08:00 +0100 |
renamed NameSpace.base to NameSpace.base_name;
|
file | diff | annotate |
| Tue, 03 Mar 2009 18:32:01 +0100 |
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;
|
file | diff | annotate |
| Mon, 09 Feb 2009 10:37:59 +0100 |
Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
|
file | diff | annotate |
| Fri, 06 Feb 2009 15:59:49 +0100 |
Merged.
|
file | diff | annotate |
| Fri, 06 Feb 2009 15:57:47 +0100 |
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
|
file | diff | annotate |
| Thu, 05 Feb 2009 14:14:03 +0100 |
code attribute applied before user attributes
|
file | diff | annotate |
| Wed, 21 Jan 2009 16:47:32 +0100 |
binding is alias for Binding.T
|
file | diff | annotate |
| Wed, 31 Dec 2008 19:54:03 +0100 |
qualified Term.rename_wrt_term;
|
file | diff | annotate |
| Wed, 31 Dec 2008 00:08:13 +0100 |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file | diff | annotate |
| Fri, 05 Dec 2008 18:43:42 +0100 |
Name.name_of -> Binding.base_name
|
file | diff | annotate |
| Thu, 04 Dec 2008 14:43:33 +0100 |
cleaned up binding module and related code
|
file | diff | annotate |
| Tue, 28 Oct 2008 16:58:59 +0100 |
cleanup code default attribute
|
file | diff | annotate |
| Tue, 07 Oct 2008 16:07:30 +0200 |
proper default codegen attribute
|
file | diff | annotate |
| Mon, 29 Sep 2008 10:58:01 +0200 |
LocalTheory.exit_global;
|
file | diff | annotate |
| Wed, 03 Sep 2008 11:44:48 +0200 |
Name.qualified;
|
file | diff | annotate |
| Tue, 02 Sep 2008 16:55:33 +0200 |
type Attrib.binding abbreviates Name.binding without attributes;
|
file | diff | annotate |
| Tue, 02 Sep 2008 14:10:45 +0200 |
explicit type Name.binding for higher-specification elements;
|
file | diff | annotate |
| Fri, 20 Jun 2008 21:00:25 +0200 |
fixed bind error for malformed primrec specifications
|
file | diff | annotate |
| Wed, 16 Apr 2008 10:57:46 +0200 |
Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).
|
file | diff | annotate |
| Fri, 04 Apr 2008 13:40:23 +0200 |
prefix for equations in primrec specifications
|
file | diff | annotate |
| Mon, 25 Feb 2008 16:31:17 +0100 |
LocalTheory.set_group for user command;
|
file | diff | annotate |
| Tue, 11 Dec 2007 10:23:11 +0100 |
dropped induction rule
|
file | diff | annotate |
| Fri, 07 Dec 2007 15:07:56 +0100 |
proper treatment of code theorems for primrec
|
file | diff | annotate |
| Fri, 07 Dec 2007 08:38:50 +0100 |
tuned further
|
file | diff | annotate |
| Thu, 06 Dec 2007 16:56:00 +0100 |
fixed slip
|
file | diff | annotate |
| Thu, 06 Dec 2007 16:36:19 +0100 |
authentic primrec
|
file | diff | annotate |
| Thu, 06 Dec 2007 15:10:09 +0100 |
added new primrec package
|
file | diff | annotate |
| Sat, 06 Oct 2007 16:50:04 +0200 |
simplified interfaces for outer syntax;
|
file | diff | annotate |
| Tue, 25 Sep 2007 17:06:14 +0200 |
proper Sign operations instead of Theory aliases;
|
file | diff | annotate |
| Tue, 25 Sep 2007 13:28:37 +0200 |
Syntax.parse/check/read;
|
file | diff | annotate |
| Tue, 18 Sep 2007 07:36:15 +0200 |
distinction between regular and default code theorems
|
file | diff | annotate |
| Thu, 30 Aug 2007 22:35:34 +0200 |
replaced ProofContext.infer_types by general Syntax.check_terms;
|
file | diff | annotate |
| Wed, 11 Jul 2007 11:44:51 +0200 |
Function unify_consts moved from OldInductivePackage to PrimrecPackage.
|
file | diff | annotate |
| Wed, 18 Apr 2007 21:30:14 +0200 |
simplified ProofContext.infer_types(_pats);
|
file | diff | annotate |
| Sun, 15 Apr 2007 14:31:49 +0200 |
proper ProofContext.infer_types;
|
file | diff | annotate |
| Tue, 20 Mar 2007 15:52:37 +0100 |
switched exception from arbitrary to undefined
|
file | diff | annotate |
| Fri, 19 Jan 2007 22:08:08 +0100 |
moved parts of OuterParse to SpecParse;
|
file | diff | annotate |
| Fri, 20 Oct 2006 10:44:47 +0200 |
fold cleanup
|
file | diff | annotate |
| Fri, 13 Oct 2006 18:23:37 +0200 |
Moved old inductive package to old_inductive_package.ML
|
file | diff | annotate |
| Mon, 02 Oct 2006 23:01:00 +0200 |
added gen_primrec
|
file | diff | annotate |
| Fri, 21 Jul 2006 14:46:27 +0200 |
exported equation transformator
|
file | diff | annotate |
| Sat, 08 Jul 2006 12:54:33 +0200 |
Goal.prove_global;
|
file | diff | annotate |
| Sat, 20 May 2006 23:36:57 +0200 |
added syntax for 'unchecked';
|
file | diff | annotate |
| Sat, 13 May 2006 02:51:49 +0200 |
added add_primrec_unchecked_i;
|
file | diff | annotate |
| Wed, 15 Feb 2006 21:34:55 +0100 |
removed distinct, renamed gen_distinct to distinct;
|
file | diff | annotate |
| Tue, 07 Feb 2006 19:56:45 +0100 |
renamed gen_duplicates to duplicates;
|
file | diff | annotate |
| Mon, 06 Feb 2006 11:01:28 +0100 |
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
|
file | diff | annotate |
| Sat, 21 Jan 2006 23:02:14 +0100 |
simplified type attribute;
|
file | diff | annotate |
| Sat, 14 Jan 2006 22:25:34 +0100 |
generic attributes;
|
file | diff | annotate |