# HG changeset patch
# User paulson
# Date 972315423 -7200
# Node ID 8627da9246da147d29f027564ac2e0fba1860a7e
# Parent  b5fe1ab860fc6469e0bcf60439478b380b81ed43
auto gen

diff -r b5fe1ab860fc -r 8627da9246da doc-src/TutorialI/Inductive/document/AB.tex
--- a/doc-src/TutorialI/Inductive/document/AB.tex	Mon Oct 23 17:36:09 2000 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Mon Oct 23 17:37:03 2000 +0200
@@ -21,13 +21,13 @@
 At the end we say a few words about the relationship of the formalization
 and the text in the book~\cite[p.\ 81]{HopcroftUllman}.
 
-We start by fixing the alpgabet, which consists only of \isa{a}'s
+We start by fixing the alphabet, which consists only of \isa{a}'s
 and \isa{b}'s:%
 \end{isamarkuptext}%
 \isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b%
 \begin{isamarkuptext}%
 \noindent
-For convenience we includ the following easy lemmas as simplification rules:%
+For convenience we include the following easy lemmas as simplification rules:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymnoteq}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}x\ {\isasymnoteq}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline
diff -r b5fe1ab860fc -r 8627da9246da doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Oct 23 17:36:09 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Oct 23 17:37:03 2000 +0200
@@ -183,7 +183,7 @@
 \end{isabelle}
 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
 ignored most of the time, or simply treated as a list of variables local to
-this subgoal. Their deeper significance is explained in Chapter~\ref{ch:Rules}.
+this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
 The {\it assumptions} are the local assumptions for this subgoal and {\it
   conclusion} is the actual proposition to be proved. Typical proof steps
 that add new assumptions are induction or case distinction. In our example