--- a/doc-src/TutorialI/CTL/CTL.thy Mon Jan 29 19:24:17 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy Mon Jan 29 22:25:45 2001 +0100
@@ -110,8 +110,10 @@
txt{*\noindent
In contrast to the analogous property for @{term EF}, and just
for a change, we do not use fixed point induction but a weaker theorem,
-@{thm[source]lfp_lowerbound}:
-@{thm[display]lfp_lowerbound[of _ "S",no_vars]}
+also known in the literature (after David Park) as \emph{Park-induction}:
+\begin{center}
+@{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound})
+\end{center}
The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
a decision that clarification takes for us:
*};
--- a/doc-src/TutorialI/CTL/document/CTL.tex Mon Jan 29 19:24:17 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Mon Jan 29 22:25:45 2001 +0100
@@ -64,10 +64,10 @@
\noindent
In contrast to the analogous property for \isa{EF}, and just
for a change, we do not use fixed point induction but a weaker theorem,
-\isa{lfp{\isacharunderscore}lowerbound}:
-\begin{isabelle}%
-\ \ \ \ \ f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S%
-\end{isabelle}
+also known in the literature (after David Park) as \emph{Park-induction}:
+\begin{center}
+\isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
+\end{center}
The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
a decision that clarification takes for us:%
\end{isamarkuptxt}%
--- a/doc-src/TutorialI/todo.tobias Mon Jan 29 19:24:17 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias Mon Jan 29 22:25:45 2001 +0100
@@ -35,6 +35,8 @@
Minor fixes in the tutorial
===========================
+warning: simp of asms from l to r; may require reordering (rotate_tac)
+
Adjust FP textbook refs: new Bird, Hudak
Discrete math textbook: Rosen?