# HG changeset patch
# User wenzelm
# Date 1518260112 -3600
# Node ID f3a68e350ab6022ff8fa9e5b6349e71656642396
# Parent  5fcd6aad8e6b638655d12c0f2bdb7e8a93fb8b66
more accessible src/Pure/ROOT.ML;

diff -r 5fcd6aad8e6b -r f3a68e350ab6 etc/settings
--- a/etc/settings	Sat Feb 10 11:19:28 2018 +0100
+++ b/etc/settings	Sat Feb 10 11:55:12 2018 +0100
@@ -105,7 +105,7 @@
 ISABELLE_DOCS="$ISABELLE_HOME/doc"
 
 ISABELLE_DOCS_RELEASE_NOTES="ANNOUNCE:README:NEWS:COPYRIGHT:CONTRIBUTORS:contrib/README:src/Tools/jEdit/README:README_REPOSITORY"
-ISABELLE_DOCS_EXAMPLES="src/HOL/ex/Seq.thy:src/HOL/ex/ML.thy:src/HOL/Unix/Unix.thy:src/HOL/Isar_Examples/Drinker.thy:src/Tools/SML/Examples.thy"
+ISABELLE_DOCS_EXAMPLES="src/HOL/ex/Seq.thy:src/HOL/ex/ML.thy:src/HOL/Unix/Unix.thy:src/HOL/Isar_Examples/Drinker.thy:src/Tools/SML/Examples.thy:src/Pure/ROOT.ML"
 
 # "open" within desktop environment (potentially asynchronous)
 case "$ISABELLE_PLATFORM_FAMILY" in
diff -r 5fcd6aad8e6b -r f3a68e350ab6 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Feb 10 11:19:28 2018 +0100
+++ b/src/Pure/ROOT.ML	Sat Feb 10 11:55:12 2018 +0100
@@ -1,3 +1,13 @@
+(*  Title:      Pure/ROOT.ML
+    Author:     Makarius
+
+Main entry point for the Isabelle/Pure bootstrap process.
+
+Note: When this file is open in the Prover IDE, the ML files of
+Isabelle/Pure can be explored interactively. This is a separate copy of
+Pure within Pure: it does not affect the running logic session.
+*)
+
 chapter "Isabelle/Pure bootstrap";
 
 ML_file "ML/ml_name_space.ML";