--- a/doc-src/TutorialI/Advanced/document/simp.tex Wed Jan 10 11:07:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Wed Jan 10 11:08:29 2001 +0100
@@ -177,6 +177,7 @@
}
%
\begin{isamarkuptext}%
+\label{sec:simp-preprocessor}
When some theorem is declared a simplification rule, it need not be a
conditional equation already. The simplifier will turn it into a set of
conditional equations automatically. For example, given \isa{f\ x\ {\isacharequal}\ g\ x\ {\isasymand}\ h\ x\ {\isacharequal}\ k\ x} the simplifier will turn this into the two separate
@@ -193,7 +194,8 @@
\end{eqnarray}
Once this conversion process is finished, all remaining non-equations
$P$ are turned into trivial equations $P = True$.
-For example, the formula \isa{{\isacharparenleft}p\ {\isasymlongrightarrow}\ q\ {\isasymand}\ r{\isacharparenright}\ {\isasymand}\ s} is converted into the three rules
+For example, the formula \begin{center}\isa{{\isacharparenleft}p\ {\isasymlongrightarrow}\ q\ {\isasymand}\ r{\isacharparenright}\ {\isasymand}\ s}\end{center}
+is converted into the three rules
\begin{center}
\isa{p\ {\isasymLongrightarrow}\ q\ {\isacharequal}\ True},\quad \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ True},\quad \isa{s\ {\isacharequal}\ True}.
\end{center}
--- a/doc-src/TutorialI/Advanced/simp.thy Wed Jan 10 11:07:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/simp.thy Wed Jan 10 11:08:29 2001 +0100
@@ -157,7 +157,7 @@
subsubsection{*The preprocessor*}
-text{*
+text{*\label{sec:simp-preprocessor}
When some theorem is declared a simplification rule, it need not be a
conditional equation already. The simplifier will turn it into a set of
conditional equations automatically. For example, given @{prop"f x =
@@ -175,7 +175,8 @@
\end{eqnarray}
Once this conversion process is finished, all remaining non-equations
$P$ are turned into trivial equations $P = True$.
-For example, the formula @{prop"(p \<longrightarrow> q \<and> r) \<and> s"} is converted into the three rules
+For example, the formula \begin{center}@{prop"(p \<longrightarrow> q \<and> r) \<and> s"}\end{center}
+is converted into the three rules
\begin{center}
@{prop"p \<Longrightarrow> q = True"},\quad @{prop"p \<Longrightarrow> r = True"},\quad @{prop"s = True"}.
\end{center}
--- a/doc-src/TutorialI/CTL/CTLind.thy Wed Jan 10 11:07:11 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTLind.thy Wed Jan 10 11:08:29 2001 +0100
@@ -128,7 +128,7 @@
@{thm[display]Avoid_in_lfp[no_vars]}
The main theorem is simply the corollary where @{prop"t = s"},
in which case the assumption @{prop"t \<in> Avoid s A"} is trivially true
-by the first @{term Avoid}-rule). Isabelle confirms this:
+by the first @{term Avoid}-rule. Isabelle confirms this:
*}
theorem AF_lemma2:
--- a/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jan 10 11:07:11 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jan 10 11:08:29 2001 +0100
@@ -125,7 +125,7 @@
\end{isabelle}
The main theorem is simply the corollary where \isa{t\ {\isacharequal}\ s},
in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
-by the first \isa{Avoid}-rule). Isabelle confirms this:%
+by the first \isa{Avoid}-rule. Isabelle confirms this:%
\end{isamarkuptext}%
\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\isanewline
\ \ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
--- a/doc-src/TutorialI/Types/Axioms.thy Wed Jan 10 11:07:11 2001 +0100
+++ b/doc-src/TutorialI/Types/Axioms.thy Wed Jan 10 11:08:29 2001 +0100
@@ -43,7 +43,8 @@
txt{*\noindent
The conclusion is not simply @{prop"\<not> y << x"} because the preprocessor
-of the simplifier would turn this into @{prop"y << x = False"}, thus yielding
+of the simplifier (see \S\ref{sec:simp-preprocessor})
+would turn this into @{prop"y << x = False"}, thus yielding
a nonterminating rewrite rule. In the above form it is a generally useful
rule.
The type constraint is necessary because otherwise Isabelle would only assume
--- a/doc-src/TutorialI/Types/document/Axioms.tex Wed Jan 10 11:07:11 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Jan 10 11:08:29 2001 +0100
@@ -45,7 +45,8 @@
\begin{isamarkuptxt}%
\noindent
The conclusion is not simply \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the preprocessor
-of the simplifier would turn this into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, thus yielding
+of the simplifier (see \S\ref{sec:simp-preprocessor})
+would turn this into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, thus yielding
a nonterminating rewrite rule. In the above form it is a generally useful
rule.
The type constraint is necessary because otherwise Isabelle would only assume
--- a/doc-src/TutorialI/todo.tobias Wed Jan 10 11:07:11 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Wed Jan 10 11:08:29 2001 +0100
@@ -75,6 +75,8 @@
Minor additions to the tutorial, unclear where
==============================================
+case_tac on bool?
+
Tacticals: , ? +
Note: + is used in typedef section!