| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Sun, 16 May 2010 00:02:11 +0200 |
wenzelm |
prefer structure Parse_Spec;
|
file |
diff |
annotate
|
| Wed, 12 May 2010 15:25:58 +0200 |
wenzelm |
updated/unified some legacy warnings;
|
file |
diff |
annotate
|
| Fri, 12 Mar 2010 12:14:30 +0100 |
bulwahn |
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 13:48:13 +0100 |
haftmann |
tuned primrec signature: return definienda
|
file |
diff |
annotate
|
| Wed, 20 Jan 2010 18:02:22 +0100 |
bulwahn |
added registration of equational theorems from prim_rec and rec_def to Spec_Rules
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 11:42:49 +0100 |
haftmann |
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 08:41:10 +0100 |
haftmann |
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 14:46:33 +0100 |
wenzelm |
adapted Local_Theory.define -- eliminated odd thm kind;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:54 +0100 |
bulwahn |
concealing internal definitions of primrec specifications
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 14:51:57 +0100 |
wenzelm |
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 17:25:09 +0100 |
wenzelm |
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 15:33:35 +0100 |
wenzelm |
removed unused Quickcheck_RecFun_Simps;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 19:21:34 +0100 |
wenzelm |
name space groups are identified by serial, not serial_string;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 17:34:35 +0200 |
blanchet |
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 18:10:39 +0200 |
haftmann |
corrected handling of free variables in arguments
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
| Sun, 21 Jun 2009 08:38:58 +0200 |
haftmann |
simplified names of common datatype types
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
| base
|