1.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Sat Jan 06 11:27:09 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Sat Jan 06 12:39:05 2001 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4  "s \<Turnstile> Neg f   = (~(s \<Turnstile> f))"
     1.5  "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
     1.6  "s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
     1.7 -"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)"
     1.8 +"s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)"
     1.9  (*>*)
    1.10  "s \<Turnstile> AF f    = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)";
    1.11  
    1.12 @@ -62,7 +62,7 @@
    1.13  "mc(Neg f)   = -mc f"
    1.14  "mc(And f g) = mc f \<inter> mc g"
    1.15  "mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
    1.16 -"mc(EF f)    = lfp(\<lambda>T. mc f \<union> M^-1 ``` T)"(*>*)
    1.17 +"mc(EF f)    = lfp(\<lambda>T. mc f \<union> M\<inverse> ``` T)"(*>*)
    1.18  "mc(AF f)    = lfp(af(mc f))";
    1.19  
    1.20  text{*\noindent
    1.21 @@ -75,12 +75,12 @@
    1.22  apply blast;
    1.23  done
    1.24  (*<*)
    1.25 -lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ``` T)";
    1.26 +lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> ``` T)";
    1.27  apply(rule monoI);
    1.28  by(blast);
    1.29  
    1.30  lemma EF_lemma:
    1.31 -  "lfp(\<lambda>T. A \<union> M^-1 ``` T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}";
    1.32 +  "lfp(\<lambda>T. A \<union> M\<inverse> ``` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}";
    1.33  apply(rule equalityI);
    1.34   apply(rule subsetI);
    1.35   apply(simp);
    1.36 @@ -366,7 +366,7 @@
    1.37  Note that @{term EU} is not definable in terms of the other operators!
    1.38  
    1.39  Model checking @{term EU} is again a least fixed point construction:
    1.40 -@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M^-1 ``` T))"}
    1.41 +@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M\<inverse> ``` T))"}
    1.42  
    1.43  \begin{exercise}
    1.44  Extend the datatype of formulae by the above until operator
    1.45 @@ -382,7 +382,7 @@
    1.46  (*<*)
    1.47  constdefs
    1.48   eufix :: "state set \<Rightarrow> state set \<Rightarrow> state set \<Rightarrow> state set"
    1.49 -"eufix A B T \<equiv> B \<union> A \<inter> (M^-1 ``` T)"
    1.50 +"eufix A B T \<equiv> B \<union> A \<inter> (M\<inverse> ``` T)"
    1.51  
    1.52  lemma "lfp(eufix A B) \<subseteq> eusem A B"
    1.53  apply(rule lfp_lowerbound)