1.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Mon Jan 29 19:24:17 2001 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Mon Jan 29 22:25:45 2001 +0100
     1.3 @@ -110,8 +110,10 @@
     1.4  txt{*\noindent
     1.5  In contrast to the analogous property for @{term EF}, and just
     1.6  for a change, we do not use fixed point induction but a weaker theorem,
     1.7 -@{thm[source]lfp_lowerbound}:
     1.8 -@{thm[display]lfp_lowerbound[of _ "S",no_vars]}
     1.9 +also known in the literature (after David Park) as \emph{Park-induction}:
    1.10 +\begin{center}
    1.11 +@{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound})
    1.12 +\end{center}
    1.13  The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
    1.14  a decision that clarification takes for us:
    1.15  *};

     2.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Mon Jan 29 19:24:17 2001 +0100
     2.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Mon Jan 29 22:25:45 2001 +0100
     2.3 @@ -64,10 +64,10 @@
     2.4  \noindent
     2.5  In contrast to the analogous property for \isa{EF}, and just
     2.6  for a change, we do not use fixed point induction but a weaker theorem,
     2.7 -\isa{lfp{\isacharunderscore}lowerbound}:
     2.8 -\begin{isabelle}%
     2.9 -\ \ \ \ \ f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S%
    2.10 -\end{isabelle}
    2.11 +also known in the literature (after David Park) as \emph{Park-induction}:
    2.12 +\begin{center}
    2.13 +\isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
    2.14 +\end{center}
    2.15  The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
    2.16  a decision that clarification takes for us:%
    2.17  \end{isamarkuptxt}%

     3.1 --- a/doc-src/TutorialI/todo.tobias	Mon Jan 29 19:24:17 2001 +0100
     3.2 +++ b/doc-src/TutorialI/todo.tobias	Mon Jan 29 22:25:45 2001 +0100
     3.3 @@ -35,6 +35,8 @@
     3.4  Minor fixes in the tutorial
     3.5  ===========================
     3.6  
     3.7 +warning: simp of asms from l to r; may require reordering (rotate_tac)
     3.8 +
     3.9  Adjust FP textbook refs: new Bird, Hudak
    3.10  Discrete math textbook: Rosen?
    3.11