# HG changeset patch
# User nipkow
# Date 1030115447 -7200
# Node ID 36ee816b5ee3568b2d09fd5eb41f2e31f7707d38
# Parent  a0749ce05100b28b88319e425216d3e465a55992
*** empty log message ***

diff -r a0749ce05100 -r 36ee816b5ee3 doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Fri Aug 23 11:08:01 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Fri Aug 23 17:10:47 2002 +0200
@@ -133,15 +133,18 @@
 This is too much proof text. Elimination rules should be selected
 automatically based on their major premise, the formula or rather connective
 to be eliminated. In Isar they are triggered by propositions being fed
-\emph{into} a proof block. Syntax:
+\emph{into} a proof. Syntax:
 \begin{center}
-\isakeyword{from} \emph{fact} \isakeyword{show} \emph{proposition}
+\isakeyword{from} \emph{fact} \isakeyword{show} \emph{proposition} \emph{proof}
 \end{center}
 where \emph{fact} stands for the name of a previously proved
 proposition, e.g.\ an assumption, an intermediate result or some global
-theorem. The fact may also be modified with @{text of}, @{text OF} etc.
-This command applies an elimination rule (from a predefined list)
-whose first premise is solved by the fact. Thus: *}
+theorem, which may also be modified with @{text of}, @{text OF} etc.
+The \emph{fact} is ``piped'' into the \emph{proof}, which can deal with it
+how it choses. If the \emph{proof} starts with a plain \isakeyword{proof},
+an elimination rule (from a predefined list) is applied
+whose first premise is solved by the \emph{fact}. Thus the proof above
+is equivalent to the following one: *}
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
@@ -210,7 +213,7 @@
 again using the facts to prove the premises.
 \end{itemize}
 In this case, the proof succeeds with @{thm[source]conjI}. Note that the proof
-would fail if we had written \isakeyword{from}~@{text"a b"}
+would fail had we written \isakeyword{from}~@{text"a b"}
 instead of \isakeyword{from}~@{text"b a"}.
 
 This treatment of facts fed into a proof is not restricted to implicit
@@ -477,8 +480,9 @@
 text{*\noindent Of course this only works in the context of HOL's carefully
 constructed introduction and elimination rules for set theory.
 
-Finally, whole scripts may appear in the leaves of the proof tree, although
-this is best avoided.  Here is a contrived example: *}
+Finally, whole ``scripts'' (unstructured proofs in the style of
+\cite{LNCS2283}) may appear in the leaves of the proof tree, although this is
+best avoided.  Here is a contrived example: *}
 
 lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B"
 proof
diff -r a0749ce05100 -r 36ee816b5ee3 doc-src/TutorialI/IsarOverview/Isar/document/root.tex
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Fri Aug 23 11:08:01 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Fri Aug 23 17:10:47 2002 +0200
@@ -37,7 +37,8 @@
 
 {\small
 \paragraph{Acknowledgment}
-I am deeply indebted to Markus Wenzel for conceiving Isar. Stefan Berghofer,
+I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin,
+Stefan Berghofer,
 Gerwin Klein, Norbert Schirmer and Markus Wenzel commented on this document.
 }