# HG changeset patch
# User wenzelm
# Date 972926880 -3600
# Node ID c20f78a9606f5d569f1ceeda9d1c504eae55bdcc
# Parent  807992b67eddeb80c858a416c42b29b70445563f
updated;

diff -r 807992b67edd -r c20f78a9606f doc-src/AxClass/generated/isabellesym.sty
--- 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
diff -r 807992b67edd -r c20f78a9606f doc-src/TutorialI/CTL/document/PDL.tex
--- 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}%
diff -r 807992b67edd -r c20f78a9606f doc-src/TutorialI/isabellesym.sty
--- 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