src/Pure/ROOT.ML
changeset 62912 745d31e63c21
parent 62911 78e03d8bf1c4
child 62918 2fcbd4abc021
     1.1 --- a/src/Pure/ROOT.ML	Thu Apr 07 21:39:03 2016 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Thu Apr 07 22:09:23 2016 +0200
     1.3 @@ -1,9 +1,9 @@
     1.4 -(*** Isabelle/Pure bootstrap ***)
     1.5 +chapter "Isabelle/Pure bootstrap";
     1.6  
     1.7  ML_file "ML/ml_name_space.ML";
     1.8  
     1.9  
    1.10 -(** bootstrap phase 0: Poly/ML setup **)
    1.11 +section "Bootstrap phase 0: Poly/ML setup";
    1.12  
    1.13  ML_file "ML/ml_pervasive0.ML";
    1.14  ML_file "ML/ml_system.ML";
    1.15 @@ -22,10 +22,9 @@
    1.16  ML_file_no_debug "ML/ml_debugger.ML";
    1.17  
    1.18  
    1.19 +section "Bootstrap phase 1: towards ML within position context";
    1.20  
    1.21 -(** bootstrap phase 1: towards ML within position context *)
    1.22 -
    1.23 -(* library of general tools *)
    1.24 +subsection "Library of general tools";
    1.25  
    1.26  ML_file "General/basics.ML";
    1.27  ML_file "library.ML";
    1.28 @@ -51,9 +50,9 @@
    1.29  ML_file "ML/ml_compiler1.ML";
    1.30  
    1.31  
    1.32 -(** bootstrap phase 2: towards ML within Isar context *)
    1.33 +section "Bootstrap phase 2: towards ML within Isar context";
    1.34  
    1.35 -(* library of general tools *)
    1.36 +subsection "Library of general tools";
    1.37  
    1.38  ML_file "General/integer.ML";
    1.39  ML_file "General/stack.ML";
    1.40 @@ -83,7 +82,7 @@
    1.41  ML_file "General/graph.ML";
    1.42  
    1.43  
    1.44 -(* fundamental structures *)
    1.45 +subsection "Fundamental structures";
    1.46  
    1.47  ML_file "name.ML";
    1.48  ML_file "term.ML";
    1.49 @@ -93,7 +92,7 @@
    1.50  ML_file "config.ML";
    1.51  
    1.52  
    1.53 -(* concurrency within the ML runtime *)
    1.54 +subsection "Concurrency within the ML runtime";
    1.55  
    1.56  ML_file "ML/exn_properties.ML";
    1.57  
    1.58 @@ -117,7 +116,7 @@
    1.59  ML_file "PIDE/active.ML";
    1.60  
    1.61  
    1.62 -(* inner syntax *)
    1.63 +subsection "Inner syntax";
    1.64  
    1.65  ML_file "Syntax/type_annotation.ML";
    1.66  ML_file "Syntax/term_position.ML";
    1.67 @@ -131,7 +130,7 @@
    1.68  ML_file "Syntax/syntax.ML";
    1.69  
    1.70  
    1.71 -(* core of tactical proof system *)
    1.72 +subsection "Core of tactical proof system";
    1.73  
    1.74  ML_file "term_ord.ML";
    1.75  ML_file "term_subst.ML";
    1.76 @@ -174,7 +173,7 @@
    1.77  ML_file "assumption.ML";
    1.78  
    1.79  
    1.80 -(* Isar -- Intelligible Semi-Automated Reasoning *)
    1.81 +subsection "Isar -- Intelligible Semi-Automated Reasoning";
    1.82  
    1.83  (*ML support and global execution*)
    1.84  ML_file "ML/ml_syntax.ML";
    1.85 @@ -221,8 +220,7 @@
    1.86  ML_file "ML/ml_compiler2.ML";
    1.87  
    1.88  
    1.89 -
    1.90 -(** bootstrap phase 3: towards theory "Pure" and final ML toplevel setup *)
    1.91 +section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";
    1.92  
    1.93  (*basic proof engine*)
    1.94  ML_file "par_tactical.ML";
    1.95 @@ -297,7 +295,7 @@
    1.96  ML_file "Isar/isar_cmd.ML";
    1.97  
    1.98  
    1.99 -(* Isabelle/Isar system *)
   1.100 +subsection "Isabelle/Isar system";
   1.101  
   1.102  ML_file "System/command_line.ML";
   1.103  ML_file "System/system_channel.ML";
   1.104 @@ -307,7 +305,7 @@
   1.105  ML_file "PIDE/protocol.ML";
   1.106  
   1.107  
   1.108 -(* miscellaneous tools and packages for Pure Isabelle *)
   1.109 +subsection "Miscellaneous tools and packages for Pure Isabelle";
   1.110  
   1.111  ML_file "ML/ml_pp.ML";
   1.112  ML_file "ML/ml_antiquotations.ML";