--- 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);
--- 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}%
--- 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.