--- a/lib/Tools/emacs Fri Jun 27 15:30:57 2014 +0200
+++ b/lib/Tools/emacs Fri Jun 27 15:41:26 2014 +0200
@@ -2,7 +2,7 @@
#
# Author: Makarius
#
-# DESCRIPTION: Proof General / Emacs interface wrapper
+# DESCRIPTION: Proof General / Emacs interface wrapper -- Proof General legacy
## diagnostics
--- a/lib/Tools/findlogics Fri Jun 27 15:30:57 2014 +0200
+++ b/lib/Tools/findlogics Fri Jun 27 15:41:26 2014 +0200
@@ -2,7 +2,7 @@
#
# Author: Markus Wenzel, TU Muenchen
#
-# DESCRIPTION: collect heap names from ISABELLE_PATH
+# DESCRIPTION: collect heap names from ISABELLE_PATH -- Proof General legacy
PRG=$(basename "$0")
--- a/src/Doc/System/Misc.thy Fri Jun 27 15:30:57 2014 +0200
+++ b/src/Doc/System/Misc.thy Fri Jun 27 15:41:26 2014 +0200
@@ -318,25 +318,6 @@
*}
-section {* Getting logic images *}
-
-text {* The @{tool_def findlogics} tool traverses all directories
- specified in @{setting ISABELLE_PATH}, looking for Isabelle logic
- images. Its usage is:
-\begin{ttbox}
-Usage: isabelle findlogics
-
- Collect heap file names from ISABELLE_PATH.
-\end{ttbox}
-
- The base names of all files found on the path are printed --- sorted
- and with duplicates removed. Also note that lookup in @{setting
- ISABELLE_PATH} includes the current values of @{setting ML_SYSTEM}
- and @{setting ML_PLATFORM}. Thus switching to another ML compiler
- may change the set of logic images available.
-*}
-
-
section {* Inspecting the settings environment \label{sec:tool-getenv} *}
text {* The Isabelle settings environment --- as provided by the