# HG changeset patch
# User wenzelm
# Date 1395821944 -3600
# Node ID bf1bdf335ea01076994d0fe9968e7a9496417344
# Parent  ca090ae5f258cb77e9144606c80e14c165627275
tuned comments;

diff -r ca090ae5f258 -r bf1bdf335ea0 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Mar 26 09:13:38 2014 +0100
+++ b/src/Pure/ROOT.ML	Wed Mar 26 09:19:04 2014 +0100
@@ -1,4 +1,6 @@
-(** Pure Isabelle **)
+(*** Isabelle/Pure bootstrap from "RAW" environment ***)
+
+(** bootstrap phase 0: towards secure ML barrier *)
 
 structure Distribution =     (*filled-in by makedist*)
 struct
@@ -35,7 +37,13 @@
 use "ML/ml_lex.ML";
 use "ML/ml_parse.ML";
 use "General/secure.ML";
-(*^^^^^ end of ML bootstrap 0 ^^^^^*)
+
+
+
+(** bootstrap phase 1: towards ML within Isar context *)
+
+(* library of general tools *)
+
 use "General/integer.ML";
 use "General/stack.ML";
 use "General/queue.ML";
@@ -224,7 +232,10 @@
 (*ML with context and antiquotations*)
 use "ML/ml_context.ML";
 use "ML/ml_antiquotation.ML";
-(*^^^^^ end of ML bootstrap 1 ^^^^^*)
+
+
+
+(** bootstrap phase 2: towards Pure.thy and final ML toplevel setup *)
 
 (*basic proof engine*)
 use "Isar/proof_display.ML";