doc-src/TutorialI/Misc/simp.thy

--- a/doc-src/TutorialI/Misc/simp.thy	Fri May 30 17:03:37 2008 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy	Fri May 30 17:52:10 2008 +0200
@@ -161,8 +161,8 @@
 
 For example, given *}
 
-constdefs xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
-         "xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
+"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"
 
 text{*\noindent
 we may want to prove