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)
2.1 --- a/doc-src/TutorialI/CTL/PDL.thy Sat Jan 06 11:27:09 2001 +0100
2.2 +++ b/doc-src/TutorialI/CTL/PDL.thy Sat Jan 06 12:39:05 2001 +0100
2.3 @@ -38,13 +38,13 @@
2.4 "s \<Turnstile> Neg f = (\<not>(s \<Turnstile> f))"
2.5 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
2.6 "s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
2.7 -"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)";
2.8 +"s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)";
2.9
2.10 text{*\noindent
2.11 The first three equations should be self-explanatory. The temporal formula
2.12 @{term"AX f"} means that @{term f} is true in all next states whereas
2.13 @{term"EF f"} means that there exists some future state in which @{term f} is
2.14 -true. The future is expressed via @{text"^*"}, the transitive reflexive
2.15 +true. The future is expressed via @{text"\<^sup>*"}, the transitive reflexive
2.16 closure. Because of reflexivity, the future includes the present.
2.17
2.18 Now we come to the model checker itself. It maps a formula into the set of
2.19 @@ -58,14 +58,14 @@
2.20 "mc(Neg f) = -mc f"
2.21 "mc(And f g) = mc f \<inter> mc g"
2.22 "mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}"
2.23 -"mc(EF f) = lfp(\<lambda>T. mc f \<union> M^-1 ``` T)"
2.24 +"mc(EF f) = lfp(\<lambda>T. mc f \<union> M\<inverse> ``` T)"
2.25
2.26 text{*\noindent
2.27 Only the equation for @{term EF} deserves some comments. Remember that the
2.28 -postfix @{text"^-1"} and the infix @{text"```"} are predefined and denote the
2.29 +postfix @{text"\<inverse>"} and the infix @{text"```"} are predefined and denote the
2.30 converse of a relation and the application of a relation to a set. Thus
2.31 -@{term "M^-1 ``` T"} is the set of all predecessors of @{term T} and the least
2.32 -fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M^-1 ``` T"} is the least set
2.33 +@{term "M\<inverse> ``` T"} is the set of all predecessors of @{term T} and the least
2.34 +fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> ``` T"} is the least set
2.35 @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
2.36 find it hard to see that @{term"mc(EF f)"} contains exactly those states from
2.37 which there is a path to a state where @{term f} is true, do not worry---that
2.38 @@ -74,7 +74,7 @@
2.39 First we prove monotonicity of the function inside @{term lfp}
2.40 *}
2.41
2.42 -lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ``` T)"
2.43 +lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> ``` T)"
2.44 apply(rule monoI)
2.45 apply blast
2.46 done
2.47 @@ -87,7 +87,7 @@
2.48 *}
2.49
2.50 lemma EF_lemma:
2.51 - "lfp(\<lambda>T. A \<union> M^-1 ``` T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}"
2.52 + "lfp(\<lambda>T. A \<union> M\<inverse> ``` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
2.53
2.54 txt{*\noindent
2.55 The equality is proved in the canonical fashion by proving that each set
2.56 @@ -112,11 +112,11 @@
2.57 Having disposed of the monotonicity subgoal,
2.58 simplification leaves us with the following main goal
2.59 \begin{isabelle}
2.60 -\ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ A\ {\isasymor}\isanewline
2.61 -\ \ \ \ \ \ \ \ \ s\ {\isasymin}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}lfp\ {\isacharparenleft}{\dots}{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
2.62 -\ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
2.63 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline
2.64 +\ \ \ \ \ \ \ \ \ x\ {\isasymin}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ {\isacharparenleft}lfp\ {\isacharparenleft}\dots{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
2.65 +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
2.66 \end{isabelle}
2.67 -which is proved by @{text blast} with the help of transitivity of @{text"^*"}:
2.68 +which is proved by @{text blast} with the help of transitivity of @{text"\<^sup>*"}:
2.69 *}
2.70
2.71 apply(blast intro: rtrancl_trans);
2.72 @@ -132,13 +132,13 @@
2.73 txt{*\noindent
2.74 After simplification and clarification we are left with
2.75 @{subgoals[display,indent=0,goals_limit=1]}
2.76 -This goal is proved by induction on @{term"(s,t)\<in>M^*"}. But since the model
2.77 +This goal is proved by induction on @{term"(s,t)\<in>M\<^sup>*"}. But since the model
2.78 checker works backwards (from @{term t} to @{term s}), we cannot use the
2.79 induction theorem @{thm[source]rtrancl_induct} because it works in the
2.80 forward direction. Fortunately the converse induction theorem
2.81 @{thm[source]converse_rtrancl_induct} already exists:
2.82 @{thm[display,margin=60]converse_rtrancl_induct[no_vars]}
2.83 -It says that if @{prop"(a,b):r^*"} and we know @{prop"P b"} then we can infer
2.84 +It says that if @{prop"(a,b):r\<^sup>*"} and we know @{prop"P b"} then we can infer
2.85 @{prop"P a"} provided each step backwards from a predecessor @{term z} of
2.86 @{term b} preserves @{term P}.
2.87 *}
3.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex Sat Jan 06 11:27:09 2001 +0100
3.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Sat Jan 06 12:39:05 2001 +0100
3.3 @@ -300,7 +300,7 @@
3.4
3.5 Model checking \isa{EU} is again a least fixed point construction:
3.6 \begin{isabelle}%
3.7 -\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}%
3.8 +\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}%
3.9 \end{isabelle}
3.10
3.11 \begin{exercise}
4.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex Sat Jan 06 11:27:09 2001 +0100
4.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Sat Jan 06 12:39:05 2001 +0100
4.3 @@ -39,13 +39,13 @@
4.4 {\isachardoublequote}s\ {\isasymTurnstile}\ Neg\ f\ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymnot}{\isacharparenleft}s\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
4.5 {\isachardoublequote}s\ {\isasymTurnstile}\ And\ f\ g\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymTurnstile}\ f\ {\isasymand}\ s\ {\isasymTurnstile}\ g{\isacharparenright}{\isachardoublequote}\isanewline
4.6 {\isachardoublequote}s\ {\isasymTurnstile}\ AX\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}\isanewline
4.7 -{\isachardoublequote}s\ {\isasymTurnstile}\ EF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}%
4.8 +{\isachardoublequote}s\ {\isasymTurnstile}\ EF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}%
4.9 \begin{isamarkuptext}%
4.10 \noindent
4.11 The first three equations should be self-explanatory. The temporal formula
4.12 \isa{AX\ f} means that \isa{f} is true in all next states whereas
4.13 \isa{EF\ f} means that there exists some future state in which \isa{f} is
4.14 -true. The future is expressed via \isa{{\isacharcircum}{\isacharasterisk}}, the transitive reflexive
4.15 +true. The future is expressed via \isa{\isactrlsup {\isacharasterisk}}, the transitive reflexive
4.16 closure. Because of reflexivity, the future includes the present.
4.17
4.18 Now we come to the model checker itself. It maps a formula into the set of
4.19 @@ -58,11 +58,11 @@
4.20 {\isachardoublequote}mc{\isacharparenleft}Neg\ f{\isacharparenright}\ \ \ {\isacharequal}\ {\isacharminus}mc\ f{\isachardoublequote}\isanewline
4.21 {\isachardoublequote}mc{\isacharparenleft}And\ f\ g{\isacharparenright}\ {\isacharequal}\ mc\ f\ {\isasyminter}\ mc\ g{\isachardoublequote}\isanewline
4.22 {\isachardoublequote}mc{\isacharparenleft}AX\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ \ {\isasymlongrightarrow}\ t\ {\isasymin}\ mc\ f{\isacharbraceright}{\isachardoublequote}\isanewline
4.23 -{\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}%
4.24 +{\isachardoublequote}mc{\isacharparenleft}EF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}%
4.25 \begin{isamarkuptext}%
4.26 \noindent
4.27 Only the equation for \isa{EF} deserves some comments. Remember that the
4.28 -postfix \isa{{\isacharcircum}{\isacharminus}{\isadigit{1}}} and the infix \isa{{\isacharbackquote}{\isacharbackquote}{\isacharbackquote}} are predefined and denote the
4.29 +postfix \isa{{\isasyminverse}} and the infix \isa{{\isacharbackquote}{\isacharbackquote}{\isacharbackquote}} are predefined and denote the
4.30 converse of a relation and the application of a relation to a set. Thus
4.31 \isa{M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T} is the set of all predecessors of \isa{T} and the least
4.32 fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T} is the least set
4.33 @@ -73,7 +73,7 @@
4.34
4.35 First we prove monotonicity of the function inside \isa{lfp}%
4.36 \end{isamarkuptext}%
4.37 -\isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}\isanewline
4.38 +\isacommand{lemma}\ mono{\isacharunderscore}ef{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isachardoublequote}\isanewline
4.39 \isacommand{apply}{\isacharparenleft}rule\ monoI{\isacharparenright}\isanewline
4.40 \isacommand{apply}\ blast\isanewline
4.41 \isacommand{done}%
4.42 @@ -85,7 +85,7 @@
4.43 a separate lemma:%
4.44 \end{isamarkuptext}%
4.45 \isacommand{lemma}\ EF{\isacharunderscore}lemma{\isacharcolon}\isanewline
4.46 -\ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%
4.47 +\ \ {\isachardoublequote}lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%
4.48 \begin{isamarkuptxt}%
4.49 \noindent
4.50 The equality is proved in the canonical fashion by proving that each set
4.51 @@ -110,11 +110,11 @@
4.52 Having disposed of the monotonicity subgoal,
4.53 simplification leaves us with the following main goal
4.54 \begin{isabelle}
4.55 -\ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymin}\ A\ {\isasymor}\isanewline
4.56 -\ \ \ \ \ \ \ \ \ s\ {\isasymin}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ {\isacharparenleft}lfp\ {\isacharparenleft}{\dots}{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
4.57 -\ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
4.58 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline
4.59 +\ \ \ \ \ \ \ \ \ x\ {\isasymin}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ {\isacharparenleft}lfp\ {\isacharparenleft}\dots{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
4.60 +\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
4.61 \end{isabelle}
4.62 -which is proved by \isa{blast} with the help of transitivity of \isa{{\isacharcircum}{\isacharasterisk}}:%
4.63 +which is proved by \isa{blast} with the help of transitivity of \isa{\isactrlsup {\isacharasterisk}}:%
4.64 \end{isamarkuptxt}%
4.65 \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtrancl{\isacharunderscore}trans{\isacharparenright}%
4.66 \begin{isamarkuptxt}%
5.1 --- a/doc-src/TutorialI/appendix.tex Sat Jan 06 11:27:09 2001 +0100
5.2 +++ b/doc-src/TutorialI/appendix.tex Sat Jan 06 12:39:05 2001 +0100
5.3 @@ -89,6 +89,12 @@
5.4 \isasymInter\index{$HOL3Set2@\isasymInter|bold}&
5.5 \ttindexbold{INT}, \ttindexbold{Inter} &
5.6 \verb$\<Inter>$\\
5.7 +\isactrlsup{\isacharasterisk}\index{$HOL4star@\isactrlsup{\isacharasterisk}|bold}&
5.8 +\verb$^*$\index{$HOL4star@\verb$^$\texttt{*}|bold} &
5.9 +\verb$\<^sup>*$\\
5.10 +\isasyminverse\index{$HOL4inv@\isasyminverse|bold}&
5.11 +\verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} &
5.12 +\verb$\<inverse>$\\
5.13 \hline
5.14 \end{tabular}
5.15 \end{center}