summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 15 Jun 2013 21:07:32 +0200 | |

changeset 52409 | 47c62377be78 |

parent 52408 | fa2dc6c6c94f |

child 52410 | fb1fb867c146 |

obsolete;

src/Doc/Ref/document/thm.tex | file | annotate | diff | comparison | revisions | |

src/HOL/Tools/reflection.ML | file | annotate | diff | comparison | revisions |

--- 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 record: \begin{ttbox} @@ -28,23 +23,6 @@ Theorems involving oracles will be printed with a suffixed \verb|[!]| to point out the different quality of confidence achieved. -\medskip - -The dependencies of theorems can be viewed using the function -\ttindexbold{thm_deps}\index{theorems!dependencies}: -\begin{ttbox} -thm_deps [\(thm@1\), \(\ldots\), \(thm@n\)]; -\end{ttbox} -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 -\begin{ttbox} -ThmDeps.enable : unit -> unit -ThmDeps.disable : unit -> unit -\end{ttbox} -to set \texttt{proofs} appropriately. - \subsection{Reconstructing and checking proof terms}\label{sec:reconstruct_proofs} \index{proof terms!reconstructing} \index{proof terms!checking}