author paulson Mon, 23 Oct 2000 10:16:52 +0200 changeset 10287 9ab1671398a6 parent 10286 fdcdb8a80988 child 10288 00abecbfa46a
two spelling fixes
--- a/doc-src/TutorialI/Inductive/AB.thy	Sun Oct 22 22:23:16 2000 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Mon Oct 23 10:16:52 2000 +0200
@@ -18,14 +18,14 @@
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 @{term a}'s
+We start by fixing the alphabet, which consists only of @{term a}'s
and @{term b}'s:
*}

datatype alfa = a | b;

text{*\noindent
-For convenience we includ the following easy lemmas as simplification rules:
+For convenience we include the following easy lemmas as simplification rules:
*}

lemma [simp]: "(x \<noteq> a) = (x = b) \<and> (x \<noteq> b) = (x = a)";