# 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 "\p. s = p (0::nat) \ (\i. (p i, p(i+1)) \ M \ Q(p i))"); +apply(subgoal_tac + "\p. s = p 0 \ (\i::nat. (p i, p(i+1)) \ M \ 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\nat \ nat" -recdef (*<*)(permissive)(*>*)f "measure(\(x,y). x-y)" - "f(x,y) = (if x \ y then x else f(x,y+1))" +consts qs :: "nat list \ nat list" +recdef(*<*)(permissive)(*>*) qs "measure length" + "qs [] = []" + "qs(x#xs) = qs(filter (\y. y\x) xs) @ [x] @ qs(filter (\y. x"} 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: "\ x \ y \ 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 \ nat list" (*>*) +recdef qs "measure length" + "qs [] = []" + "qs(x#xs) = qs(filter (\y. y\x) xs) @ [x] @ qs(filter (\y. x*) +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\nat \ nat" (*>*) -recdef f "measure(\(x,y). x-y)" - "f(x,y) = (if x \ 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}