Sat, 15 Jun 2013 21:07:32 +0200
changeset 52409 47c62377be78
parent 52408 fa2dc6c6c94f
child 52410 fb1fb867c146
--- a/src/Doc/Ref/document/thm.tex	Sat Jun 15 21:01:07 2013 +0200
+++ b/src/Doc/Ref/document/thm.tex	Sat Jun 15 21:07:32 2013 +0200
@@ -3,11 +3,6 @@
 \section{Proof terms}\label{sec:proofObjects}
-Note that there are no separate constructors
-for abstraction and application on the level of {\em types}, since
-instantiation of type variables is accomplished via the type assignments
-attached to {\tt Thm}, {\tt Axm} and {\tt Oracle}.
 Each theorem's derivation is stored as the {\tt der} field of its internal
@@ -28,23 +23,6 @@
 Theorems involving oracles will be printed with a
 suffixed \verb|[!]| to point out the different quality of confidence achieved.
-The dependencies of theorems can be viewed using the function
-thm_deps [\(thm@1\), \(\ldots\), \(thm@n\)];
-generates the dependency graph of the theorems $thm@1$, $\ldots$, $thm@n$ and
-displays it using Isabelle's graph browser. For this to work properly,
-the theorems in question have to be proved with {\tt proofs} set to a value
-greater than {\tt 0}. You can use
-ThmDeps.enable : unit -> unit
-ThmDeps.disable : unit -> unit
-to set \texttt{proofs} appropriately.
 \subsection{Reconstructing and checking proof terms}\label{sec:reconstruct_proofs}
 \index{proof terms!reconstructing}
 \index{proof terms!checking}