diff -r 4dc65845eab3 -r d8d7d1b785af doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -365,8 +365,7 @@
 *}
 
 (*<*)
-constdefs
- eufix :: "state set \<Rightarrow> state set \<Rightarrow> state set \<Rightarrow> state set"
+definition eufix :: "state set \<Rightarrow> state set \<Rightarrow> state set \<Rightarrow> state set" where
 "eufix A B T \<equiv> B \<union> A \<inter> (M\<inverse> `` T)"
 
 lemma "lfp(eufix A B) \<subseteq> eusem A B"
@@ -397,8 +396,7 @@
 done
 
 (*
-constdefs
- eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set"
+definition eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
 "eusem A B \<equiv> {s. \<exists>p\<in>Paths s. \<exists>j. p j \<in> B \<and> (\<forall>i < j. p i \<in> A)}"
 
 axioms
@@ -414,8 +412,7 @@
 apply(blast intro: M_total[THEN someI_ex])
 done
 
-constdefs
- pcons :: "state \<Rightarrow> (nat \<Rightarrow> state) \<Rightarrow> (nat \<Rightarrow> state)"
+definition pcons :: "state \<Rightarrow> (nat \<Rightarrow> state) \<Rightarrow> (nat \<Rightarrow> state)" where
 "pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j"
 
 lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s";