# HG changeset patch
# User nipkow
# Date 1007039562 -3600
# Node ID 7c4ec77a8715f1231cd7962af54a3e54055ffadd
# Parent  5a4d782044924026ad49cb05fe59461073b46935
*** empty log message ***

diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Thu Nov 29 14:12:42 2001 +0100
@@ -106,7 +106,7 @@
 *};
 
 theorem AF_lemma1:
-  "lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}";
+  "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}";
 
 txt{*\noindent
 In contrast to the analogous proof for @{term EF}, and just
@@ -304,7 +304,7 @@
 At last we can prove the opposite direction of @{thm[source]AF_lemma1}:
 *};
 
-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)";
 
 txt{*\noindent
 The proof is again pointwise and then by contraposition:
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/CTL/document/CTL.tex
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Thu Nov 29 14:12:42 2001 +0100
@@ -98,7 +98,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
+\ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent
@@ -342,7 +342,7 @@
 At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma{\isadigit{1}}}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\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}\isamarkupfalse%
+\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}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/Inductive/Even.thy
--- a/doc-src/TutorialI/Inductive/Even.thy	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Even.thy	Thu Nov 29 14:12:42 2001 +0100
@@ -21,7 +21,7 @@
 
 Our first lemma states that numbers of the form $2\times k$ are even. *}
 lemma two_times_even[intro!]: "2*k \<in> even"
-apply (induct "k")
+apply (induct_tac k)
 txt{*
 The first step is induction on the natural number \isa{k}, which leaves
 two subgoals:
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/Inductive/document/Even.tex
--- a/doc-src/TutorialI/Inductive/document/Even.tex	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/Inductive/document/Even.tex	Thu Nov 29 14:12:42 2001 +0100
@@ -34,7 +34,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ two{\isacharunderscore}times{\isacharunderscore}even{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isadigit{2}}{\isacharasterisk}k\ {\isasymin}\ even{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{apply}\ {\isacharparenleft}induct\ {\isachardoublequote}k{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}induct{\isacharunderscore}tac\ k{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 The first step is induction on the natural number \isa{k}, which leaves
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/Inductive/even-example.tex
--- a/doc-src/TutorialI/Inductive/even-example.tex	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/Inductive/even-example.tex	Thu Nov 29 14:12:42 2001 +0100
@@ -59,7 +59,7 @@
 \begin{isabelle}
 \isacommand{lemma}\ two_times_even[intro!]:\ "\#2*k\ \isasymin \ even"
 \isanewline
-\isacommand{apply}\ (induct\ "k")\isanewline
+\isacommand{apply}\ (induct_tac\ k)\isanewline
 \ \isacommand{apply}\ auto\isanewline
 \isacommand{done}
 \end{isabelle}
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Thu Nov 29 14:12:42 2001 +0100
@@ -70,7 +70,7 @@
   tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by
   others (especially the single step tactics in Chapter~\ref{chap:rules}).
   If you need the full set of numerals, see~\S\ref{sec:numerals}.
-  \emph{Novices are advised to stick to \isa{{\isadigit{0}}} and of \isa{Suc}.}
+  \emph{Novices are advised to stick to \isa{{\isadigit{0}}} and \isa{Suc}.}
 \end{warn}
 
 Both \isa{auto} and \isa{simp}
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/Trie/Trie.thy
--- a/doc-src/TutorialI/Trie/Trie.thy	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/Trie/Trie.thy	Thu Nov 29 14:12:42 2001 +0100
@@ -59,7 +59,7 @@
 
 text{*
 Things begin to get interesting with the definition of an update function
-that adds a new (string,value) pair to a trie, overwriting the old value
+that adds a new (string, value) pair to a trie, overwriting the old value
 associated with that string:
 *};
 
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/Trie/document/Trie.tex
--- a/doc-src/TutorialI/Trie/document/Trie.tex	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Thu Nov 29 14:12:42 2001 +0100
@@ -69,7 +69,7 @@
 %
 \begin{isamarkuptext}%
 Things begin to get interesting with the definition of an update function
-that adds a new (string,value) pair to a trie, overwriting the old value
+that adds a new (string, value) pair to a trie, overwriting the old value
 associated with that string:%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Thu Nov 29 14:12:42 2001 +0100
@@ -412,7 +412,7 @@
 In HOL it must be ruled out because it requires a type
 \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
 same cardinality --- an impossibility. For the same reason it is not possible
-to allow recursion involving the type \isa{set}, which is isomorphic to
+to allow recursion involving the type \isa{t set}, which is isomorphic to
 \isa{t \isasymFun\ bool}.
 
 Fortunately, a limited form of recursion
diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Thu Nov 29 14:12:42 2001 +0100
@@ -1,5 +1,7 @@
 "You know my methods. Apply them!"
 
+Explain indentation of apply's
+
 Implementation
 ==============