diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Readme.thy --- 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{\}"} & @{text "\\isccite{\}"}\\ - Isar Reference Manual & @{text "\\rchcite{\}"} & @{text "\\rsccite{\}"}\\ - \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] "\"} 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,\)\"}"} - \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,\)"} - \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 \\"}"} - \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 "\ \ \"} - 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 "\ \ \"} - 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