tuned comments;
authorwenzelm
Wed Mar 26 09:19:04 2014 +0100 (2014-03-26)
changeset 56288bf1bdf335ea0
parent 56287 ca090ae5f258
child 56289 d8d2a2b97168
child 56291 e79f76a48449
tuned comments;
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Wed Mar 26 09:13:38 2014 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed Mar 26 09:19:04 2014 +0100
     1.3 @@ -1,4 +1,6 @@
     1.4 -(** Pure Isabelle **)
     1.5 +(*** Isabelle/Pure bootstrap from "RAW" environment ***)
     1.6 +
     1.7 +(** bootstrap phase 0: towards secure ML barrier *)
     1.8  
     1.9  structure Distribution =     (*filled-in by makedist*)
    1.10  struct
    1.11 @@ -35,7 +37,13 @@
    1.12  use "ML/ml_lex.ML";
    1.13  use "ML/ml_parse.ML";
    1.14  use "General/secure.ML";
    1.15 -(*^^^^^ end of ML bootstrap 0 ^^^^^*)
    1.16 +
    1.17 +
    1.18 +
    1.19 +(** bootstrap phase 1: towards ML within Isar context *)
    1.20 +
    1.21 +(* library of general tools *)
    1.22 +
    1.23  use "General/integer.ML";
    1.24  use "General/stack.ML";
    1.25  use "General/queue.ML";
    1.26 @@ -224,7 +232,10 @@
    1.27  (*ML with context and antiquotations*)
    1.28  use "ML/ml_context.ML";
    1.29  use "ML/ml_antiquotation.ML";
    1.30 -(*^^^^^ end of ML bootstrap 1 ^^^^^*)
    1.31 +
    1.32 +
    1.33 +
    1.34 +(** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
    1.35  
    1.36  (*basic proof engine*)
    1.37  use "Isar/proof_display.ML";