# HG changeset patch
# User nipkow
# Date 1008258514 -3600
# Node ID c92e38c3cbaa44c61a9c8596b1446b1450fbeefc
# Parent  83acab8042add8bb290c895b398d38ef0618e280
*** empty log message ***

diff -r 83acab8042ad -r c92e38c3cbaa NEWS
--- a/NEWS	Thu Dec 13 16:48:07 2001 +0100
+++ b/NEWS	Thu Dec 13 16:48:34 2001 +0100
@@ -1,4 +1,3 @@
-
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
@@ -224,6 +223,10 @@
 a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be
 necessary to attach explicit type constraints;
 
+* HOL/Relation: the prefix name of the infix "O" has been changed from "comp"
+to "rel_comp"; INCOMPATIBILITY: a few theorems have been renamed accordingly
+(eg "compI" -> "rel_compI").
+
 * HOL: syntax translations now work properly with numerals and records
 expressions;
 
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Thu Dec 13 16:48:34 2001 +0100
@@ -203,7 +203,8 @@
 both the path property and the fact that @{term Q} holds:
 *};
 
-apply(subgoal_tac "\<exists>p. s = p (0::nat) \<and> (\<forall>i. (p i, p(i+1)) \<in> M \<and> Q(p i))");
+apply(subgoal_tac
+  "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))");
 
 txt{*\noindent
 From this proposition the original goal follows easily:
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/CTL/document/CTL.tex
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Thu Dec 13 16:48:34 2001 +0100
@@ -221,7 +221,8 @@
 both the path property and the fact that \isa{Q} holds:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
+\ \ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharcolon}{\isacharcolon}nat{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Thu Dec 13 16:48:34 2001 +0100
@@ -25,7 +25,7 @@
 are explained in \S\ref{sec:SimpHow}.
 
 The simplification attribute of theorems can be turned on and off:%
-\index{*simp del (attribute)}\REMARK{need to index attributes!switching off??}
+\index{*simp del (attribute)}
 \begin{quote}
 \isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp{\isacharbrackright}}\\
 \isacommand{declare} \textit{theorem-name}\isa{{\isacharbrackleft}simp\ del{\isacharbrackright}}
@@ -237,7 +237,7 @@
 There is also the special method \isa{unfold}\index{*unfold (method)|bold}
 which merely unfolds
 one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
-This is can be useful if \isa{simp} does too much.%
+This is can be useful in situations where \isa{simp} does too much.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Thu Dec 13 16:48:34 2001 +0100
@@ -21,7 +21,7 @@
 are explained in \S\ref{sec:SimpHow}.
 
 The simplification attribute of theorems can be turned on and off:%
-\index{*simp del (attribute)}\REMARK{need to index attributes!switching off??}
+\index{*simp del (attribute)}
 \begin{quote}
 \isacommand{declare} \textit{theorem-name}@{text"[simp]"}\\
 \isacommand{declare} \textit{theorem-name}@{text"[simp del]"}
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Thu Dec 13 16:48:34 2001 +0100
@@ -15,55 +15,56 @@
 simplification rules.
 
 Isabelle may fail to prove the termination condition for some
-recursive call.  Let us try the following artificial function:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
-\isamarkupfalse%
-\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-\noindent This definition fails, and Isabelle prints an error message
-showing you what it was unable to prove. You will then have to prove it as a
-separate lemma before you attempt the definition of your function once
-more. In our case the required lemma is the obvious one:%
+recursive call.  Let us try to define Quicksort:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-It was not proved automatically because of the awkward behaviour of subtraction
-on type \isa{nat}. This requires more arithmetic than is tried by default:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
+\isacommand{consts}\ qs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ list\ {\isasymRightarrow}\ nat\ list{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{done}\isamarkupfalse%
+\isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
+\ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
+\ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-\noindent
-Because \isacommand{recdef}'s termination prover involves simplification,
-we include in our second attempt a hint: the \attrdx{recdef_simp} attribute 
-says to use \isa{termi{\isacharunderscore}lem} as a simplification rule.%
+\noindent where \isa{filter} is predefined and \isa{filter\ P\ xs}
+is the list of elements of \isa{xs} satisfying \isa{P}.
+This definition of \isa{qs} fails, and Isabelle prints an error message
+showing you what it was unable to prove:
+\begin{isabelle}%
+\ \ \ \ \ length\ {\isacharparenleft}filter\ {\isachardot}{\isachardot}{\isachardot}\ xs{\isacharparenright}\ {\isacharless}\ Suc\ {\isacharparenleft}length\ xs{\isacharparenright}%
+\end{isabelle}
+We can either prove this as a separate lemma, or try to figure out which
+existing lemmas may help. We opt for the second alternative. The theory of
+lists contains the simplification rule \isa{length\ {\isacharparenleft}filter\ P\ xs{\isacharparenright}\ {\isasymle}\ length\ xs},
+which is already
+close to what we need, except that we still need to turn \mbox{\isa{{\isacharless}\ Suc}}
+into
+\isa{{\isasymle}} for the simplification rule to apply. Lemma
+\isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} does just that: \isa{{\isacharparenleft}m\ {\isacharless}\ Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}m\ {\isasymle}\ n{\isacharparenright}}.
+
+Now we retry the above definition but supply the lemma(s) just found (or
+proved). Because \isacommand{recdef}'s termination prover involves
+simplification, we include in our second attempt a hint: the
+\attrdx{recdef_simp} attribute says to use \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} as a
+simplification rule.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
 \isamarkupfalse%
-\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
-{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}\isamarkupfalse%
+\isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
+\ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
+\ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isanewline
+{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
-This time everything works fine. Now \isa{f{\isachardot}simps} contains precisely
-the stated recursion equation for \isa{f}, which has been turned into a
-simplification rule.  Thus we can automatically prove results such as this one:%
+This time everything works fine. Now \isa{qs{\isachardot}simps} contains precisely
+the stated recursion equations for \isa{qs} and they have become
+simplification rules.
+Thus we can automatically prove results such as this one:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{theorem}\ {\isachardoublequote}f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{theorem}\ {\isachardoublequote}qs{\isacharbrackleft}{\isadigit{2}}{\isacharcomma}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharbrackright}\ {\isacharequal}\ qs{\isacharbrackleft}{\isadigit{3}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{2}}{\isacharbrackright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
 \isamarkupfalse%
@@ -73,10 +74,10 @@
 \noindent
 More exciting theorems require induction, which is discussed below.
 
-If the termination proof requires a new lemma that is of general use, you can
+If the termination proof requires a lemma that is of general use, you can
 turn it permanently into a simplification rule, in which case the above
-\isacommand{hint} is not necessary. But our \isa{termi{\isacharunderscore}lem} is not
-sufficiently general to warrant this distinction.%
+\isacommand{hint} is not necessary. But in the case of
+\isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} this would be of dubious value.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/Recdef/termination.thy
--- a/doc-src/TutorialI/Recdef/termination.thy	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/Recdef/termination.thy	Thu Dec 13 16:48:34 2001 +0100
@@ -14,55 +14,57 @@
 simplification rules.
 
 Isabelle may fail to prove the termination condition for some
-recursive call.  Let us try the following artificial function:*}
+recursive call.  Let us try to define Quicksort:*}
 
-consts f :: "nat\<times>nat \<Rightarrow> nat"
-recdef (*<*)(permissive)(*>*)f "measure(\<lambda>(x,y). x-y)"
-  "f(x,y) = (if x \<le> y then x else f(x,y+1))"
+consts qs :: "nat list \<Rightarrow> nat list"
+recdef(*<*)(permissive)(*>*) qs "measure length"
+ "qs [] = []"
+ "qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)"
 
-text{*\noindent This definition fails, and Isabelle prints an error message
-showing you what it was unable to prove. You will then have to prove it as a
-separate lemma before you attempt the definition of your function once
-more. In our case the required lemma is the obvious one: *}
+text{*\noindent where @{term filter} is predefined and @{term"filter P xs"}
+is the list of elements of @{term xs} satisfying @{term P}.
+This definition of @{term qs} fails, and Isabelle prints an error message
+showing you what it was unable to prove:
+@{text[display]"length (filter ... xs) < Suc (length xs)"}
+We can either prove this as a separate lemma, or try to figure out which
+existing lemmas may help. We opt for the second alternative. The theory of
+lists contains the simplification rule @{thm length_filter[no_vars]},
+which is already
+close to what we need, except that we still need to turn \mbox{@{text"< Suc"}}
+into
+@{text"\<le>"} for the simplification rule to apply. Lemma
+@{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}.
 
-lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y"
+Now we retry the above definition but supply the lemma(s) just found (or
+proved). Because \isacommand{recdef}'s termination prover involves
+simplification, we include in our second attempt a hint: the
+\attrdx{recdef_simp} attribute says to use @{thm[source]less_Suc_eq_le} as a
+simplification rule.  *}
 
-txt{*\noindent
-It was not proved automatically because of the awkward behaviour of subtraction
-on type @{typ"nat"}. This requires more arithmetic than is tried by default:
+(*<*)global consts qs :: "nat list \<Rightarrow> nat list" (*>*)
+recdef qs "measure length"
+ "qs [] = []"
+ "qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)"
+(hints recdef_simp: less_Suc_eq_le)
+(*<*)local(*>*)
+text{*\noindent
+This time everything works fine. Now @{thm[source]qs.simps} contains precisely
+the stated recursion equations for @{text qs} and they have become
+simplification rules.
+Thus we can automatically prove results such as this one:
 *}
 
-apply(arith)
-done
-
-text{*\noindent
-Because \isacommand{recdef}'s termination prover involves simplification,
-we include in our second attempt a hint: the \attrdx{recdef_simp} attribute 
-says to use @{thm[source]termi_lem} as a simplification rule.  
-*}
-
-(*<*)global consts f :: "nat\<times>nat \<Rightarrow> nat" (*>*)
-recdef f "measure(\<lambda>(x,y). x-y)"
-  "f(x,y) = (if x \<le> y then x else f(x,y+1))"
-(hints recdef_simp: termi_lem)
-(*<*)local(*>*)
-text{*\noindent
-This time everything works fine. Now @{thm[source]f.simps} contains precisely
-the stated recursion equation for @{text f}, which has been turned into a
-simplification rule.  Thus we can automatically prove results such as this one:
-*}
-
-theorem "f(1,0) = f(1,1)"
+theorem "qs[2,3,0] = qs[3,0,2]"
 apply(simp)
 done
 
 text{*\noindent
 More exciting theorems require induction, which is discussed below.
 
-If the termination proof requires a new lemma that is of general use, you can
+If the termination proof requires a lemma that is of general use, you can
 turn it permanently into a simplification rule, in which case the above
-\isacommand{hint} is not necessary. But our @{thm[source]termi_lem} is not
-sufficiently general to warrant this distinction.
+\isacommand{hint} is not necessary. But in the case of
+@{thm[source]less_Suc_eq_le} this would be of dubious value.
 *}
 (*<*)
 end
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/Sets/Relations.thy
--- a/doc-src/TutorialI/Sets/Relations.thy	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/Sets/Relations.thy	Thu Dec 13 16:48:34 2001 +0100
@@ -12,8 +12,8 @@
 *}
 
 text{*
-@{thm[display] comp_def[no_vars]}
-\rulename{comp_def}
+@{thm[display] rel_comp_def[no_vars]}
+\rulename{rel_comp_def}
 *}
 
 text{*
@@ -22,8 +22,8 @@
 *}
 
 text{*
-@{thm[display] comp_mono[no_vars]}
-\rulename{comp_mono}
+@{thm[display] rel_comp_mono[no_vars]}
+\rulename{rel_comp_mono}
 *}
 
 text{*
@@ -32,8 +32,8 @@
 *}
 
 text{*
-@{thm[display] converse_comp[no_vars]}
-\rulename{converse_comp}
+@{thm[display] converse_rel_comp[no_vars]}
+\rulename{converse_rel_comp}
 *}
 
 text{*
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Thu Dec 13 16:48:34 2001 +0100
@@ -670,7 +670,7 @@
 available: 
 \begin{isabelle}
 r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright
-\rulenamedx{comp_def}
+\rulenamedx{rel_comp_def}
 \end{isabelle}
 %
 This is one of the many lemmas proved about these concepts: 
@@ -686,7 +686,7 @@
 \isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\
 \isasymsubseteq\ s\isasymrbrakk\ \isasymLongrightarrow\ r\isacharprime\ O\
 s\isacharprime\ \isasymsubseteq\ r\ O\ s%
-\rulename{comp_mono}
+\rulename{rel_comp_mono}
 \end{isabelle}
 
 \indexbold{converse!of a relation}%
@@ -704,7 +704,7 @@
 Here is a typical law proved about converse and composition: 
 \begin{isabelle}
 (r\ O\ s)\isasyminverse\ =\ s\isasyminverse\ O\ r\isasyminverse
-\rulename{converse_comp}
+\rulename{converse_rel_comp}
 \end{isabelle}
 
 \indexbold{image!under a relation}%
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/appendix.tex
--- a/doc-src/TutorialI/appendix.tex	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/appendix.tex	Thu Dec 13 16:48:34 2001 +0100
@@ -115,7 +115,7 @@
 
 \begin{table}[htbp]
 \begin{center}
-\begin{tabular}{|lllllllll|}
+\begin{tabular}{@{}|lllllllll|@{}}
 \hline
 \texttt{ALL} &
 \texttt{BIT} &
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/preface.tex
--- a/doc-src/TutorialI/preface.tex	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/preface.tex	Thu Dec 13 16:48:34 2001 +0100
@@ -36,4 +36,3 @@
 GR\slash K77051, GR\slash M75440, GR\slash R01156\slash 01 and by the
 \textsc{esprit} working groups 21900 and IST-1999-29001 (the \emph{Types}
 project).
-
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Thu Dec 13 16:48:34 2001 +0100
@@ -3,28 +3,10 @@
 Implementation
 ==============
 
-- (#2 * x) = #2 * - x is not proved by arith
+Add map_cong?? (upto 10% slower)
 
 a simp command for terms
 
-----------------------------------------------------------------------
-primrec 
-"(foorec [] []) = []"
-"(foorec [] (y # ys)) = (y # (foorec [] ys))"
-
-*** Primrec definition error:
-*** extra variables on rhs: "y", "ys"
-*** in
-*** "((foorec [] ((y::'a_1) # (ys::'a_1 list))) = (y # (foorec [] ys)))"
-*** At command "primrec".
-
-Bessere Fehlermeldung!
-----------------------------------------------------------------------
-
-Relation: comp -> composition
-
-Add map_cong?? (upto 10% slower)
-
 Recdef: Get rid of function name in header.
 Support mutual recursion (Konrad?)
 
@@ -33,9 +15,6 @@
 better 1 point rules:
 !x. !y. x = f y --> P x y  should reduce to  !y. P (f y) y.
 
-use arith_tac in recdef to solve termination conditions?
--> new example in Recdef/termination
-
 it would be nice if @term could deal with ?-vars.
 then a number of (unchecked!) @texts could be converted to @terms.
 
diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/tutorial.tex	Thu Dec 13 16:48:34 2001 +0100
@@ -69,10 +69,18 @@
 \input{Advanced/advanced}
 \input{Protocol/protocol}
 
-%\chapter{Structured Proofs}
-%\label{ch:Isar}
-%\chapter{Case Study: UNIX File-System Security}
-%\chapter{The Tricks of the Trade}
+\markboth{}{}
+\cleardoublepage
+\vspace*{\fill}
+\begin{flushright}
+\begin{tabular}{l}
+{\large\sf\slshape You know my methods. Apply them!}\\[1ex]
+Sherlock Holmes
+\end{tabular}
+\end{flushright}
+\vspace*{\fill}
+\vspace*{\fill}
+
 \input{appendix}
 
 \bibliographystyle{plain}