| #
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
| #
e195e62f |
|
09-Apr-2016 |
wenzelm <none@none> |
clarified modules;
|
| #
cd156ec4 |
|
07-Apr-2016 |
wenzelm <none@none> |
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;
|
| #
fda5e1b6 |
|
07-Apr-2016 |
wenzelm <none@none> |
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
|
| #
2bef420f |
|
07-Apr-2016 |
wenzelm <none@none> |
clarified bootstrap of @{make_string} -- avoid query on ML environment;
|
| #
37f57172 |
|
06-Apr-2016 |
wenzelm <none@none> |
more robust bootstrap;
|
| #
ff7c1b69 |
|
06-Apr-2016 |
wenzelm <none@none> |
simplified bootstrap: critical structures remain accessible in ML_Root context;
|
| #
fe36f207 |
|
05-Apr-2016 |
wenzelm <none@none> |
avoid malformed Isabelle symbols during bootstrap;
|
| #
33f46939 |
|
02-Apr-2016 |
wenzelm <none@none> |
tuned signature;
|
| #
fd5f3b5a |
|
02-Apr-2016 |
wenzelm <none@none> |
careful export of type-dependent functions, without losing their special status;
|
| #
2d17444f |
|
02-Apr-2016 |
wenzelm <none@none> |
clarified modules;
|
| #
b38efe8a |
|
26-Mar-2016 |
wenzelm <none@none> |
explicit print_depth for the sake of Spec_Check.determine_type;
|
| #
fc0cde3e |
|
18-Mar-2016 |
wenzelm <none@none> |
discontinued slightly odd "secure" mode;
|
| #
f0caccd4 |
|
17-Mar-2016 |
wenzelm <none@none> |
@{make_string} is available during Pure bootstrap;
|
| #
9b94c25b |
|
06-Mar-2016 |
wenzelm <none@none> |
clarified treatment of fragments of Isabelle symbols during bootstrap;
|
| #
866c57fc |
|
03-Mar-2016 |
wenzelm <none@none> |
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
--HG--
rename : src/Pure/RAW/multithreading.ML => src/Pure/Concurrent/multithreading.ML
rename : src/Pure/RAW/unsynchronized.ML => src/Pure/Concurrent/unsynchronized.ML
rename : src/Pure/RAW/exn.ML => src/Pure/General/exn.ML
rename : src/Pure/RAW/exn.scala => src/Pure/General/exn.scala
rename : src/Pure/RAW/secure.ML => src/Pure/General/secure.ML
rename : src/Pure/RAW/fixed_int_dummy.ML => src/Pure/ML/fixed_int_dummy.ML
rename : src/Pure/RAW/ml_compiler0.ML => src/Pure/ML/ml_compiler0.ML
rename : src/Pure/RAW/ml_debugger.ML => src/Pure/ML/ml_debugger.ML
rename : src/Pure/RAW/ml_heap.ML => src/Pure/ML/ml_heap.ML
rename : src/Pure/RAW/ml_name_space.ML => src/Pure/ML/ml_name_space.ML
rename : src/Pure/RAW/ml_pretty.ML => src/Pure/ML/ml_pretty.ML
rename : src/Pure/RAW/ml_profiling.ML => src/Pure/ML/ml_profiling.ML
rename : src/Pure/RAW/ml_system.ML => src/Pure/ML/ml_system.ML
|