Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/IsarImplementation/Integration.thy
changeset 56265 785569927666
parent 55838 e120a15b0ee6 
--- a/src/Doc/IsarImplementation/Integration.thy	Sun Mar 23 16:40:35 2014 +0100
+++ b/src/Doc/IsarImplementation/Integration.thy	Mon Mar 24 12:00:17 2014 +0100
@@ -52,7 +52,6 @@
   @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
   @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
   @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
-  @{index_ML Toplevel.debug: "bool Unsynchronized.ref"} \\
   @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
   @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
   \end{mldecls}
@@ -79,9 +78,6 @@
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
   state if available, otherwise raises @{ML Toplevel.UNDEF}.
 
-  \item @{ML "Toplevel.debug := true"} enables exception trace of the
-  ML runtime system.
-
   \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.
isabelle