| Sat, 09 Apr 2016 14:00:23 +0200 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 11:21:38 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 22:09:23 +0200 |
wenzelm |
section headings for ROOT.ML;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 21:39:03 +0200 |
wenzelm |
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 20:51:52 +0200 |
wenzelm |
clarified mode of ROOT.ML files;
|
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
|
| Thu, 07 Apr 2016 11:17:57 +0200 |
wenzelm |
clarified editor mode;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 19:03:29 +0200 |
wenzelm |
virtual thread data via context, for proper support of Context.>> etc;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 16:51:52 +0200 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 16:33:33 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2016 11:37:37 +0200 |
wenzelm |
clarified ML bootstrap;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 21:51:14 +0200 |
wenzelm |
clarified files;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 21:23:32 +0200 |
wenzelm |
back to static conditional compilation -- simplified bootstrap;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:51:37 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 18:25:42 +0200 |
wenzelm |
actually observe ML_system_unsafe, concerning the environment that is stored in theory ML_Root;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 17:25:11 +0200 |
wenzelm |
prefer antiquotations;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 17:16:46 +0200 |
wenzelm |
proper use_thy;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 23:58:48 +0200 |
wenzelm |
more uniform ML file commands;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 20:46:39 +0200 |
wenzelm |
clarified bootstrap -- avoid conditional compilation in ROOT.ML;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 20:28:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 20:20:47 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 19:48:54 +0200 |
wenzelm |
clarified conditional compilation;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 17:25:53 +0200 |
wenzelm |
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 17:02:34 +0200 |
wenzelm |
clarified bootstrap -- more uniform use of ML files;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 16:14:22 +0200 |
wenzelm |
clarified bootstrap;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 15:53:56 +0200 |
wenzelm |
clarified final setup of ML environment;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 15:35:24 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 23:14:08 +0200 |
wenzelm |
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 20:33:34 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 20:23:51 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|