--- a/CookBook/Readme.thy Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,159 +0,0 @@
-theory Readme
-imports Base
-begin
-
-chapter {* Comments for Authors *}
-
-text {*
-
- \begin{itemize}
- \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 tutorial. Some parts of the tutorial also rely on compilation with
- PolyML.
-
- \item You can include references to other Isabelle manuals using the
- reference names from those manuals. To do this the following
- four \LaTeX{} commands are defined:
-
- \begin{center}
- \begin{tabular}{l|c|c}
- & Chapters & Sections\\\hline
- Implementation Manual & @{text "\\ichcite{\<dots>}"} & @{text "\\isccite{\<dots>}"}\\
- Isar Reference Manual & @{text "\\rchcite{\<dots>}"} & @{text "\\rsccite{\<dots>}"}\\
- \end{tabular}
- \end{center}
-
- So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic
- in the implementation manual, namely \ichcite{ch:logic}.
-
- \item There are various document antiquotations defined for the
- 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.
-
- The following antiquotations are defined:
-
- \begin{itemize}
- \item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used
- for displaying any ML-ex\-pression, because the antiquotation checks whether
- the expression is valid ML-code. The @{text "for"}- and @{text
- "in"}-arguments are optional. The former is used for evaluating open
- expressions by giving a list of free variables. The latter is used to
- indicate in which structure or structures the ML-expression should be
- evaluated. Examples are:
-
- \begin{center}\small
- \begin{tabular}{lll}
- @{text "@{ML \"1 + 3\"}"} & & @{ML "1 + 3"}\\
- @{text "@{ML \"a + b\" for a b}"} & \;\;produce\;\; & @{ML "a + b" for a b}\\
- @{text "@{ML Ident in OuterLex}"} & & @{ML Ident in OuterLex}\\
- \end{tabular}
- \end{center}
-
- \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to
- display ML-expressions and their response. The first expression is checked
- like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern
- that specifies the result the first expression produces. This pattern can
- contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the
- first expression will be checked against this pattern. Examples are:
-
- \begin{center}\small
- \begin{tabular}{l}
- @{text "@{ML_response \"1+2\" \"3\"}"}\\
- @{text "@{ML_response \"(1+2,3)\" \"(3,\<dots>)\"}"}
- \end{tabular}
- \end{center}
-
- which produce respectively
-
- \begin{center}\small
- \begin{tabular}{p{3cm}p{3cm}}
- @{ML_response "1+2" "3"} &
- @{ML_response "(1+2,3)" "(3,\<dots>)"}
- \end{tabular}
- \end{center}
-
- Note that this antiquotation can only be used when the result can be
- constructed: it does not work when the code produces an exception or returns
- an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
-
- \item[$\bullet$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just
- like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above,
- except that the result-specification is not checked. Use this antiquotation
- when the result cannot be constructed or the code generates an
- exception. Examples are:
-
- \begin{center}\small
- \begin{tabular}{ll}
- @{text "@{ML_response_fake"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\
- & @{text "\"a + b = c\"}"}\smallskip\\
- @{text "@{ML_response_fake"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\
- & @{text "\"Exception FAIL raised\"}"}
- \end{tabular}
- \end{center}
-
- which produce respectively
-
- \begin{center}\small
- \begin{tabular}{p{7.2cm}}
- @{ML_response_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\
- @{ML_response_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}
- \end{tabular}
- \end{center}
-
- This output mimics to some extend what the user sees when running the
- code.
-
- \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be
- used to show erroneous code. Neither the code nor the response will be
- checked. An example is:
-
- \begin{center}\small
- \begin{tabular}{ll}
- @{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\
- & @{text "\"Type unification failed \<dots>\"}"}
- \end{tabular}
- \end{center}
-
- \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when
- referring to a file. It checks whether the file exists. An example
- is
-
- @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}
- \end{itemize}
-
- The listed antiquotations honour options including @{text "[display]"} and
- @{text "[quotes]"}. For example
-
- \begin{center}\small
- @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"}
- \end{center}
-
- whereas
-
- \begin{center}\small
- @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}
- \end{center}
-
- \item Functions and value bindings cannot be defined inside antiquotations; they need
- to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
- environments. In this way they are also checked by the compiler. Some \LaTeX-hack in
- the tutorial, however, ensures that the environment markers are not printed.
-
- \item Line numbers can be printed using
- \isacommand{ML} \isa{\%linenos}~@{text "\<verbopen> \<dots> \<verbclose>"}
- for ML-code or \isacommand{lemma} \isa{\%linenos} @{text "..."} for proofs. The
- tag is \isa{\%linenosgray} when the numbered text should be gray.
-
- \end{itemize}
-
-*}
-
-
-
-end
\ No newline at end of file