diff -r b5914f3c643c -r 5b9c6010897b CookBook/Readme.thy --- a/CookBook/Readme.thy Wed Dec 17 05:08:33 2008 +0000 +++ b/CookBook/Readme.thy Sat Jan 03 20:44:54 2009 +0000 @@ -7,14 +7,14 @@ text {* \begin{itemize} - \item The cookbook can be compiled on the command-line with: + \item The Cookbook can be compiled on the command-line with: \begin{center} @{text "isabelle make"} \end{center} You very likely need a recent snapshot of Isabelle in order to compile - the cookbook. + the Cookbook. \item You can include references to other Isabelle manuals using the reference names from those manuals. To do this the following @@ -32,7 +32,7 @@ in the implementation manual, namely \ichcite{ch:logic}. \item There are various document antiquotations defined for the - cookbook. They allow to check the written text against the current + Cookbook. They allow to check the written text against the current Isabelle code and also allow to show responses of the ML-compiler. Therefore authors are strongly encouraged to use antiquotations wherever appropriate.