| Sat, 30 May 2009 08:17:05 +0200 |
haftmann |
simps with mandatory name prefix
|
file |
diff |
annotate
|
| Wed, 27 May 2009 22:11:06 +0200 |
haftmann |
tuned signature of add_primrec_simple
|
file |
diff |
annotate
|
| Tue, 26 May 2009 17:29:34 +0200 |
haftmann |
add_primrec_simple
|
file |
diff |
annotate
|
| Mon, 18 May 2009 09:48:06 +0200 |
haftmann |
introduced Thm.generatedK
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Sat, 16 May 2009 15:23:52 +0200 |
bulwahn |
added collection of simplification rules of recursive functions for quickcheck
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 21:55:02 +0100 |
wenzelm |
simplified preparation and outer parsing of specification;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 19:27:48 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:56:52 +0100 |
haftmann |
corrected type inference of primitive definitions
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:42:19 +0100 |
wenzelm |
explicit Binding.qualified_name -- prevents implicitly qualified bstring;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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.
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 15:59:49 +0100 |
blanchet |
Merged.
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 15:57:47 +0100 |
blanchet |
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 14:14:03 +0100 |
haftmann |
code attribute applied before user attributes
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 19:54:03 +0100 |
wenzelm |
qualified Term.rename_wrt_term;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Tue, 28 Oct 2008 16:58:59 +0100 |
haftmann |
cleanup code default attribute
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:30 +0200 |
haftmann |
proper default codegen attribute
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 10:58:01 +0200 |
wenzelm |
LocalTheory.exit_global;
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 11:44:48 +0200 |
wenzelm |
Name.qualified;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 21:00:25 +0200 |
haftmann |
fixed bind error for malformed primrec specifications
|
file |
diff |
annotate
|
| Wed, 16 Apr 2008 10:57:46 +0200 |
berghofe |
Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).
|
file |
diff |
annotate
|