# HG changeset patch # User Christian Urban # Date 1234142615 0 # Node ID bdd82350cf226003703372cc89526a92cdc73a43 # Parent f49dc7e962357e5622ed88adaca2bd3e2c520fc4 renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious) diff -r f49dc7e96235 -r bdd82350cf22 CookBook/Base.thy --- a/CookBook/Base.thy Mon Feb 09 01:12:00 2009 +0000 +++ b/CookBook/Base.thy Mon Feb 09 01:23:35 2009 +0000 @@ -10,7 +10,7 @@ val _ = OuterSyntax.command "ML" "eval ML text within theory" - (OuterKeyword.tag "CookBookML" OuterKeyword.thy_decl) + (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) (OuterParse.ML_source >> (fn (txt, pos) => Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); *} diff -r f49dc7e96235 -r bdd82350cf22 CookBook/Intro.thy --- a/CookBook/Intro.thy Mon Feb 09 01:12:00 2009 +0000 +++ b/CookBook/Intro.thy Mon Feb 09 01:23:35 2009 +0000 @@ -8,19 +8,19 @@ text {* If your next project requires you to program on the ML-level of Isabelle, - then this Cookbook is for you. It will guide you through the first steps of + then this tutorial is for you. It will guide you through the first steps of Isabelle programming, and also explain tricks of the trade. The best way to get to know the ML-level of Isabelle is by experimenting with the many code - examples included in the Cookbook. The code is as far as possible checked + examples included in the tutorial. The code is as far as possible checked against recent versions of Isabelle. If something does not work, then please let us know. If you have comments, criticism or like to add to the - Cookbook, feel free---you are most welcome! + tutorial, feel free---you are most welcome! *} section {* Intended Audience and Prior Knowledge *} text {* - This Cookbook targets readers who already know how to use Isabelle for + This tutorial targets readers who already know how to use Isabelle for writing theories and proofs. We also assume that readers are familiar with the functional programming language ML, the language in which most of Isabelle is implemented. If you are unfamiliar with either of these two @@ -68,7 +68,7 @@ text {* - All ML-code in this Cookbook is typeset in highlighted boxes, like the following + All ML-code in this tutorial is typeset in highlighted boxes, like the following ML-expression: \begin{isabelle} diff -r f49dc7e96235 -r bdd82350cf22 CookBook/Readme.thy --- a/CookBook/Readme.thy Mon Feb 09 01:12:00 2009 +0000 +++ b/CookBook/Readme.thy Mon Feb 09 01:23:35 2009 +0000 @@ -7,12 +7,12 @@ text {* \begin{itemize} - \item The Cookbook can be compiled on the command-line with: + \item This tutorial can be compiled on the command-line with: @{text [display] "$ isabelle make"} You very likely need a recent snapshot of Isabelle in order to compile - the Cookbook. Some parts of the Cookbook also rely on compilation with + the tutorial. Some parts of the tutorial also rely on compilation with PolyML. \item You can include references to other Isabelle manuals using the @@ -31,7 +31,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 + tutorial. 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. @@ -143,7 +143,7 @@ \item Functions and value bindings cannot be defined inside antiquotations; they need to be included inside \isacommand{ML}~@{text "\ \ \"} environments. In this way they are also checked by the compiler. Some \LaTeX-hack in - the Cookbook, however, ensures that the environment markers are not printed. + the tutorial, however, ensures that the environment markers are not printed. \item Line numbers can be printed using \isacommand{ML} \isa{\%linenumbers}~@{text "\ \ \"} diff -r f49dc7e96235 -r bdd82350cf22 CookBook/antiquote_setup.ML --- a/CookBook/antiquote_setup.ML Mon Feb 09 01:12:00 2009 +0000 +++ b/CookBook/antiquote_setup.ML Mon Feb 09 01:23:35 2009 +0000 @@ -1,4 +1,4 @@ -(* Auxiliary antiquotations for the Cookbook. *) +(* Auxiliary antiquotations for the tutorial. *) structure AntiquoteSetup: sig end = struct diff -r f49dc7e96235 -r bdd82350cf22 CookBook/document/root.tex --- a/CookBook/document/root.tex Mon Feb 09 01:12:00 2009 +0000 +++ b/CookBook/document/root.tex Mon Feb 09 01:23:35 2009 +0000 @@ -78,9 +78,9 @@ \renewcommand{\isacharverbatimopen}{}% \renewcommand{\isacharverbatimclose}{}}{} -\isakeeptag{CookBookML} -\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}} -\renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}} +\isakeeptag{TutorialML} +\renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}} +\renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % for code that has line numbers @@ -103,7 +103,7 @@ \title{\mbox{}\\[-10ex] \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] - The Isabelle Programmer's Cookbook (fragment)} + The Isabelle Programming Tutorial (fragment)} \author{with contributions by:\\[2ex] \begin{tabular}{r@{\hspace{1.8mm}}l} diff -r f49dc7e96235 -r bdd82350cf22 IsaMakefile --- a/IsaMakefile Mon Feb 09 01:12:00 2009 +0000 +++ b/IsaMakefile Mon Feb 09 01:23:35 2009 +0000 @@ -1,11 +1,11 @@ ## targets -default: cookbook +default: tutorial images: test: -all: cookbook +all: tutorial ## global settings @@ -21,7 +21,7 @@ ## CookBook -cookbook: CookBook/ROOT.ML \ +tutorial: CookBook/ROOT.ML \ CookBook/document/root.tex \ CookBook/document/root.bib \ CookBook/*.thy \ diff -r f49dc7e96235 -r bdd82350cf22 cookbook.pdf Binary file cookbook.pdf has changed