# HG changeset patch
# User nipkow
# Date 980803545 -3600
# Node ID ef0b521698b7c6f0e0497e5b4c7e6593b665378d
# Parent  9429f2e7d16a38a47ab3e8e3ff6c1f592cb97d7c
*** empty log message ***

diff -r 9429f2e7d16a -r ef0b521698b7 doc-src/TutorialI/CTL/CTL.thy
--- 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:
 *};
diff -r 9429f2e7d16a -r ef0b521698b7 doc-src/TutorialI/CTL/document/CTL.tex
--- 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}%
diff -r 9429f2e7d16a -r ef0b521698b7 doc-src/TutorialI/todo.tobias
--- 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?