author wenzelm Mon, 30 Oct 2000 18:28:00 +0100 changeset 10361 c20f78a9606f parent 10360 807992b67edd child 10362 c6b197ccf1f1
updated;
--- a/doc-src/AxClass/generated/isabellesym.sty	Mon Oct 30 18:26:14 2000 +0100
+++ b/doc-src/AxClass/generated/isabellesym.sty	Mon Oct 30 18:28:00 2000 +0100
@@ -127,7 +127,7 @@
\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
\newcommand{\isasymbar}{\isamath{\mid}}
\newcommand{\isasymhyphen}{\isatext{\rm-}}
-\newcommand{\isasymmacron}{\isatext{\rm\=\relax}}
+\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
--- a/doc-src/TutorialI/CTL/document/PDL.tex	Mon Oct 30 18:26:14 2000 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Mon Oct 30 18:28:00 2000 +0100
@@ -63,8 +63,8 @@
Only the equation for \isa{EF} deserves some comments. Remember that the
postfix \isa{{\isacharcircum}{\isacharminus}{\isadigit{1}}} and the infix \isa{{\isacharcircum}{\isacharcircum}} are predefined and denote the
converse of a relation and the application of a relation to a set. Thus
-\isa{M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the set of all predecessors of \isa{T} and the least
-fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T} is the least set
+\isa{M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T} is the set of all predecessors of \isa{T} and the least
+fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharcircum}{\isacharcircum}\ T} is the least set
\isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
which there is a path to a state where \isa{f} is true, do not worry---that
@@ -128,17 +128,17 @@
\begin{isabelle}
\ \isadigit{1}{\isachardot}\ {\isasymAnd}s\ t{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}{\isacharsemicolon}\ t\ {\isasymin}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ s\ {\isasymin}\ lfp\ {\isacharparenleft}{\isasymlambda}T{\isachardot}\ A\ {\isasymunion}\ M{\isacharcircum}{\isacharminus}\isadigit{1}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}
\end{isabelle}
-This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M{\isacharcircum}{\isacharasterisk}}. But since the model
+This goal is proved by induction on \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}}. But since the model
checker works backwards (from \isa{t} to \isa{s}), we cannot use the
induction theorem \isa{rtrancl{\isacharunderscore}induct} because it works in the
forward direction. Fortunately the converse induction theorem
\isa{converse{\isacharunderscore}rtrancl{\isacharunderscore}induct} already exists:
\begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline
-\ \ \ \ \ \ \ \ {\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}{\isacharsemicolon}\ P\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y{\isasymrbrakk}\isanewline
+\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ b{\isacharsemicolon}\isanewline
+\ \ \ \ \ \ \ \ {\isasymAnd}y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}z{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}{\isacharsemicolon}\ P\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y{\isasymrbrakk}\isanewline
\ \ \ \ \ {\isasymLongrightarrow}\ P\ a%
\end{isabelle}
-It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r{\isacharcircum}{\isacharasterisk}} and we know \isa{P\ b} then we can infer
+It says that if \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymin}\ r\isactrlsup {\isacharasterisk}} and we know \isa{P\ b} then we can infer
\isa{P\ a} provided each step backwards from a predecessor \isa{z} of
\isa{b} preserves \isa{P}.%
\end{isamarkuptxt}%
--- a/doc-src/TutorialI/isabellesym.sty	Mon Oct 30 18:26:14 2000 +0100
+++ b/doc-src/TutorialI/isabellesym.sty	Mon Oct 30 18:28:00 2000 +0100
@@ -127,7 +127,7 @@
\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
\newcommand{\isasymbar}{\isamath{\mid}}
\newcommand{\isasymhyphen}{\isatext{\rm-}}
-\newcommand{\isasymmacron}{\isatext{\rm\=\relax}}
+\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel