
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{\<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




