# HG changeset patch # User paulson # Date 972289012 -7200 # Node ID 9ab1671398a62116f082686f2a7b0a07af8bb2e7 # Parent fdcdb8a80988c17342f0f5314486b27fdb76f551 two spelling fixes diff -r fdcdb8a80988 -r 9ab1671398a6 doc-src/TutorialI/Inductive/AB.thy --- 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 \ a) = (x = b) \ (x \ b) = (x = a)";