# HG changeset patch
# User nipkow
# Date 1026278402 -7200
# Node ID 53c4ec15cae05fb0aa77882e0ab369d80a311345
# Parent  703de709a64b73ae7a8ab23f9250dfff1ab680c5
*** empty log message ***

diff -r 703de709a64b -r 53c4ec15cae0 doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Tue Jul 09 23:05:26 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Jul 10 07:20:02 2002 +0200
@@ -33,13 +33,13 @@
 Text starting with ``--'' is a comment.
 
 Note that propositions in \isakeyword{assume} may but need not be
-separated by \isakeyword{and} whose purpose is to structure the
-assumptions into possibly named blocks, for example
+separated by \isakeyword{and}, whose purpose is to structure the
+assumptions into possibly named blocks. For example in
 \begin{center}
 \isakeyword{assume} @{text"A:"} $A_1$ $A_2$ \isakeyword{and} @{text"B:"} $A_3$
 \isakeyword{and} $A_4$
 \end{center}
-Here label @{text A} refers to the list of propositions $A_1$ $A_2$ and
+label @{text A} refers to the list of propositions $A_1$ $A_2$ and
 label @{text B} to $A_3$.
 *}
 
@@ -246,13 +246,15 @@
   qed
 qed
 text{*\noindent Apart from demonstrating the strangeness of classical
-arguments by contradiction, this example also introduces three new constructs:
-\begin{itemize}
-\item \isakeyword{next} deals with multiple subgoals.  When showing
-@{term"A \<and> B"} we need to show both @{term A} and @{term B}.  Each subgoal
-is proved separately, in \emph{any} order. The individual proofs are
-separated by \isakeyword{next}.
-\end{itemize}
+arguments by contradiction, this example also introduces two new
+abbrebviations:
+\begin{center}
+\begin{tabular}{lcl}
+\isakeyword{hence} &=& \isakeyword{then} \isakeyword{have} \\
+\isakeyword{with}~\emph{facts} &=&
+\isakeyword{from}~\emph{facts} \isakeyword{and} @{text this}
+\end{tabular}
+\end{center}
 *}
 
 subsection{*Avoiding duplication*}
@@ -269,7 +271,13 @@
 text{*\noindent The \isakeyword{proof} always works on the conclusion,
 @{prop"B \<and> A"} in our case, thus selecting $\land$-introduction. Hence
 we must show @{prop B} and @{prop A}; both are proved by
-$\land$-elimination.
+$\land$-elimination and the proofs are separated by \isakeyword{next}:
+\begin{description}
+\item[\isakeyword{next}] deals with multiple subgoals. For example,
+when showing @{term"A \<and> B"} we need to show both @{term A} and @{term
+B}.  Each subgoal is proved separately, in \emph{any} order. The
+individual proofs are separated by \isakeyword{next}.
+\end{description}
 
 This is all very well as long as formulae are small. Let us now look at some
 devices to avoid repeating (possibly large) formulae. A very general method
@@ -384,9 +392,8 @@
 \isakeyword{fix} and \isakeyword{assume} together with a soundness proof of
 the elimination involved.
 
-Here is a proof of a well known tautology which employs another useful
-abbreviation: \isakeyword{hence} abbreviates \isakeyword{from}~@{text
-this}~\isakeyword{have}.  Figure out which rule is used where!  *}
+Here is a proof of a well known tautology.
+Figure out which rule is used where!  *}
 
 lemma assumes ex: "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y"
 proof
@@ -418,7 +425,7 @@
   qed
 qed
 text{*\noindent
-For a start, the example demonstrates three new language elements:
+For a start, the example demonstrates two new constructs:
 \begin{itemize}
 \item \isakeyword{let} introduces an abbreviation for a term, in our case
 the witness for the claim, because the term occurs multiple times in the proof.
@@ -426,11 +433,6 @@
 implicit what the two cases are: it is merely expected that the two subproofs
 prove @{prop"P \<Longrightarrow> Q"} and @{prop"\<not>P \<Longrightarrow> Q"} for suitable @{term P} and
 @{term Q}.
-\item \isakeyword{with} is an abbreviation:
-\begin{center}
-\isakeyword{with}~\emph{facts} \quad = \quad
-\isakeyword{from}~\emph{facts} \isakeyword{and} @{text this}
-\end{center}
 \end{itemize}
 If you wonder how to \isakeyword{obtain} @{term y}:
 via the predefined elimination rule @{thm rangeE[no_vars]}.
@@ -699,4 +701,20 @@
 see very clearly how things fit together and permit ourselves the
 obvious forward step @{text"IH[OF B]"}. *}
 
+consts rot :: "'a list \<Rightarrow> 'a list"
+recdef rot "measure length"
+"rot [] = []"
+"rot [x] = [x]"
+"rot (x#y#zs) = y # rot(x#zs)"
+
+lemma "length(rot xs) = length xs" (is "?P xs")
+proof (induct xs rule: rot.induct)
+  show "?P []" by simp
+next
+  fix x show "?P [x]" by simp
+next
+  fix x y zs assume "?P (x#zs)"
+  thus "?P (x#y#zs)" by simp
+qed
+
 (*<*)end(*>*)
diff -r 703de709a64b -r 53c4ec15cae0 doc-src/TutorialI/IsarOverview/Isar/document/root.tex
--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Tue Jul 09 23:05:26 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex	Wed Jul 10 07:20:02 2002 +0200
@@ -32,8 +32,8 @@
 %%% End:
 
 \paragraph{Acknowledgment}
-I am deeply indebted to Markus Wenzel for conceiving Isar and for
-commenting on this document.
+I am deeply indebted to Markus Wenzel for conceiving Isar. Stefan Berghofer
+and Markus Wenzel commented on this document.
 
 \begingroup
 \bibliographystyle{plain} \small\raggedright\frenchspacing