--- a/doc-src/TutorialI/CTL/PDL.thy Sat Jan 06 10:36:19 2001 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy Sat Jan 06 11:27:09 2001 +0100
@@ -58,14 +58,14 @@
"mc(Neg f) = -mc f"
"mc(And f g) = mc f \<inter> mc g"
"mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}"
-"mc(EF f) = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)"
+"mc(EF f) = lfp(\<lambda>T. mc f \<union> M^-1 ``` T)"
text{*\noindent
Only the equation for @{term EF} deserves some comments. Remember that the
-postfix @{text"^-1"} and the infix @{text"^^"} are predefined and denote the
+postfix @{text"^-1"} and the infix @{text"```"} are predefined and denote the
converse of a relation and the application of a relation to a set. Thus
-@{term "M^-1 ^^ T"} is the set of all predecessors of @{term T} and the least
-fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M^-1 ^^ T"} is the least set
+@{term "M^-1 ``` T"} is the set of all predecessors of @{term T} and the least
+fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M^-1 ``` T"} is the least set
@{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
find it hard to see that @{term"mc(EF f)"} contains exactly those states from
which there is a path to a state where @{term f} is true, do not worry---that
@@ -74,7 +74,7 @@
First we prove monotonicity of the function inside @{term lfp}
*}
-lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)"
+lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ``` T)"
apply(rule monoI)
apply blast
done
@@ -87,7 +87,7 @@
*}
lemma EF_lemma:
- "lfp(\<lambda>T. A \<union> M^-1 ^^ T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}"
+ "lfp(\<lambda>T. A \<union> M^-1 ``` T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}"
txt{*\noindent
The equality is proved in the canonical fashion by proving that each set