# HG changeset patch
# User nipkow
# Date 979127630 -3600
# Node ID 140a1ed65665b0a776f20c54c1903bcd9f32d2cc
# Parent  d1ff1ff5c5ad0b78084bea01d8c08b9fbb9d1750
*** empty log message ***

diff -r d1ff1ff5c5ad -r 140a1ed65665 doc-src/TutorialI/CTL/CTLind.thy
--- a/doc-src/TutorialI/CTL/CTLind.thy	Wed Jan 10 12:43:51 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTLind.thy	Wed Jan 10 12:53:50 2001 +0100
@@ -131,8 +131,7 @@
 by the first @{term Avoid}-rule. Isabelle confirms this:
 *}
 
-theorem AF_lemma2:
-  "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
+theorem AF_lemma2:  "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
 by(auto elim:Avoid_in_lfp intro:Avoid.intros);
 
 
diff -r d1ff1ff5c5ad -r 140a1ed65665 doc-src/TutorialI/CTL/document/CTLind.tex
--- a/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Jan 10 12:43:51 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Jan 10 12:53:50 2001 +0100
@@ -127,8 +127,7 @@
 in which case the assumption \isa{t\ {\isasymin}\ Avoid\ s\ A} is trivially true
 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
+\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\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
 \isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
 \isanewline
 \end{isabellebody}%
diff -r d1ff1ff5c5ad -r 140a1ed65665 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Wed Jan 10 12:43:51 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Wed Jan 10 12:53:50 2001 +0100
@@ -40,9 +40,6 @@
 explanation of term "contrapositive"/contraposition in Rules?
 Index the notion and maybe the rules contrapos_xy
 
-If Advanced and Types chapter ar swapped:
-Make forward ref from ... = True in Axioms to preprocessor section.
-
 get rid of use_thy in tutorial?
 
 Orderings on numbers (with hint that it is overloaded):
@@ -75,7 +72,7 @@
 Minor additions to the tutorial, unclear where
 ==============================================
 
-case_tac on bool?
+unfold?
 
 Tacticals: , ? +
 Note: + is used in typedef section!
@@ -83,10 +80,6 @@
 A list of further useful commands (rules? tricks?)
 prefer, defer, print_simpset (-> print_simps?)
 
-Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
-Where explained? Should go into a separate section as Inductive needs it as
-well.
-
 demonstrate x : set xs in Sets. Or Tricks chapter?
 
 Appendix with HOL and Isar keywords.