diff -r f42353afd6d3 -r ea48dd8b0232 doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Fri Jan 05 10:19:32 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Fri Jan 05 13:10:37 2001 +0100
@@ -136,28 +136,28 @@
 original definition. For example, given
 *}
 
-constdefs exor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
-         "exor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
+constdefs xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+         "xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)";
 
 text{*\noindent
 we may want to prove
 *}
 
-lemma "exor A (\<not>A)";
+lemma "xor A (\<not>A)";
 
 txt{*\noindent
 Typically, the opening move consists in \emph{unfolding} the definition(s), which we need to
 get started, but nothing else:\indexbold{*unfold}\indexbold{definition!unfolding}
 *}
 
-apply(simp only:exor_def);
+apply(simp only:xor_def);
 
 txt{*\noindent
 In this particular case, the resulting goal
 @{subgoals[display,indent=0]}
 can be proved by simplification. Thus we could have proved the lemma outright by
-*}(*<*)oops;lemma "exor A (\<not>A)";(*>*)
-apply(simp add: exor_def)
+*}(*<*)oops;lemma "xor A (\<not>A)";(*>*)
+apply(simp add: xor_def)
 (*<*)done(*>*)
 text{*\noindent
 Of course we can also unfold definitions in the middle of a proof.