| Mon, 30 May 2016 20:58:54 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 28 May 2016 21:38:58 +0200 |
wenzelm |
clarified 'axiomatization';
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:43:17 +0200 |
haftmann |
do not export abstract constructors in code_reflect
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
optional timing for code generator conversions
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified internal interfaces
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
corrected closure scope of static_conv_thingol;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified proof context vs. background theory
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified naming conventions and code for code evaluation sandwiches
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified names of variants
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 16:53:43 +0200 |
wenzelm |
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 16:33:33 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:03:24 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Sat, 26 Mar 2016 16:14:46 +0100 |
wenzelm |
explicit print_depth for the sake of Spec_Check.determine_type;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2016 09:06:50 +0100 |
haftmann |
dropped junk
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 22:49:33 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 22:11:36 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 21:10:29 +0100 |
wenzelm |
load secure.ML earlier;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 23:06:24 +0100 |
wenzelm |
SML/NJ is no longer supported;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 23:10:23 +0200 |
wenzelm |
thread context for exceptions from forks, e.g. relevant when printing errors;
|
file |
diff |
annotate
|
| Mon, 17 Aug 2015 16:27:12 +0200 |
wenzelm |
explicit debug flag for ML compiler;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:52:14 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 20:32:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 12:56:06 +0100 |
wenzelm |
proper exception for internal program failure, not user-error;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 12:36:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Dec 2014 19:24:54 +0100 |
wenzelm |
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 19:35:36 +0100 |
haftmann |
allow multiple inheritance of targets
|
file |
diff |
annotate
|
| Thu, 09 Oct 2014 22:43:48 +0200 |
haftmann |
more foundational definition for predicate even
|
file |
diff |
annotate
|