Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed deriv;
authorwenzelm
Tue, 12 Jan 1999 15:39:34 +0100
changeset 6097 04515352f19e
parent 6096 3451f9e88528
child 6098 8648c6651f07
fixed deriv;
doc-src/Ref/thm.tex file | annotate | diff | comparison | revisions 
--- a/doc-src/Ref/thm.tex	Tue Jan 12 15:25:53 1999 +0100
+++ b/doc-src/Ref/thm.tex	Tue Jan 12 15:39:34 1999 +0100
@@ -773,7 +773,7 @@
 record: 
 \begin{ttbox} 
 #der (rep_thm conjI);
-{\out Join (Theorem "HOL.conjI", [Join (MinProof,[])]) : deriv}
+{\out Join (Theorem ("HOL.conjI", []), [Join (MinProof,[])]) : deriv}
 \end{ttbox}
 This proof object identifies a labelled theorem, {\tt conjI} of theory
 \texttt{HOL}, whose underlying proof has not been recorded; all we
isabelle