# HG changeset patch
# User nipkow
# Date 927281473 -7200
# Node ID 8a1b5f9d842096abe4c6b9fed84d521f9ef00440
# Parent  acbcf8085166574f13f98ece04d5d9092c24ef19
qed indexed.

diff -r acbcf8085166 -r 8a1b5f9d8420 doc-src/Tutorial/basics.tex
--- a/doc-src/Tutorial/basics.tex	Fri May 21 11:48:42 1999 +0200
+++ b/doc-src/Tutorial/basics.tex	Fri May 21 12:11:13 1999 +0200
@@ -245,9 +245,10 @@
 
 Most of the time you can and should ignore unknowns and work with ordinary
 variables. Just don't be surprised that after you have finished the
-proof of a theorem, Isabelle will turn your free variables into unknowns: it
-merely indicates that Isabelle will automatically instantiate those unknowns
-suitably when the theorem is used in some other proof.
+proof of a theorem, Isabelle (i.e.\ \ttindex{qed} at the end of a proof) will
+turn your free variables into unknowns: it merely indicates that Isabelle will
+automatically instantiate those unknowns suitably when the theorem is used in
+some other proof.
 \begin{warn}
   The existential quantifier \texttt{?}\index{$HOLQ@{\tt?}} needs to be
   followed by a space. Otherwise \texttt{?x} is interpreted as a schematic
diff -r acbcf8085166 -r 8a1b5f9d8420 doc-src/Tutorial/fp.tex
--- a/doc-src/Tutorial/fp.tex	Fri May 21 11:48:42 1999 +0200
+++ b/doc-src/Tutorial/fp.tex	Fri May 21 12:11:13 1999 +0200
@@ -219,7 +219,7 @@
 \end{ttbox}
 Now we can give the lemma just proved a suitable name
 \begin{ttbox}
-\input{ToyList/qed2}\end{ttbox}
+\input{ToyList/qed2}\end{ttbox}\index{*qed}
 and tell Isabelle to use this lemma in all future proofs by simplification:
 \begin{ttbox}
 \input{ToyList/addsimps2}\end{ttbox}
@@ -854,7 +854,7 @@
   is like \verb$Simp_tac$, but extracts additional rewrite rules from
   the assumptions of the subgoal. For example, it solves
 \begin{ttbox}\makeatother
-{\out 1. xs = [] ==> xs @ xs = xs}
+{\out 1. xs = [] ==> xs @ ys = ys @ xs}
 \end{ttbox}
 which \texttt{Simp_tac} does not do.