| Wed, 10 Dec 2014 19:24:54 +0100 |
wenzelm |
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sat, 19 Apr 2014 17:23:05 +0200 |
wenzelm |
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 13:18:10 +0100 |
wenzelm |
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 13:36:28 +0100 |
wenzelm |
clarified bootstrap process: switch to ML with context and antiquotations earlier;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2012 11:48:45 +0200 |
wenzelm |
renamed Position.str_of to Position.here;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 12:51:37 +0200 |
wenzelm |
proper masking of dummy name_space;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 11:39:08 +0200 |
wenzelm |
proper checking of ML functors (in Poly/ML 5.2 or later);
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Sat, 06 Jun 2009 18:11:32 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 17:31:39 +0200 |
wenzelm |
eliminated costly registration of tokens;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 23:28:04 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 16:12:42 +0200 |
wenzelm |
maintain tokens within common ML environment;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 15:26:00 +0200 |
wenzelm |
moved local ML environment to separate module ML_Env;
|
file |
diff |
annotate
|