--- 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:
--- 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
--- 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:
--- 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
--- 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}
--- 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}
--- 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:
*};
--- 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%
--- 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
--- 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
==============