theory Readme+
−
imports Base+
−
begin+
−
+
−
chapter \<open>Comments for Authors\<close>+
−
+
−
text \<open>+
−
+
−
  \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 & \<open>\ichcite{\<dots>}\<close> & \<open>\isccite{\<dots>}\<close>\\+
−
  Isar Reference Manual & \<open>\rchcite{\<dots>}\<close> & \<open>\rsccite{\<dots>}\<close>\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  So \<open>\ichcite{ch:logic}\<close> 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$] \<open>@{ML "expr" for vars in structs}\<close> should be used+
−
  for displaying any ML-ex\-pression, because the antiquotation checks whether+
−
  the expression is valid ML-code. The \<open>for\<close>- and \<open>in\<close>-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}+
−
  \<open>@{ML "1 + 3"}\<close>         &                 & @{ML "1 + 3"}\\+
−
  \<open>@{ML "a + b" for a b}\<close> & \;\;produce\;\; & @{ML "a + b" for a b}\\+
−
  \<open>@{ML Ident in OuterLex}\<close> &                 & @{ML Ident in OuterLex}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \item[$\bullet$] \<open>@{ML_response "expr" "pat"}\<close> should be used to+
−
  display ML-expressions and their response.  The first expression is checked+
−
  like in the antiquotation \<open>@{ML "expr"}\<close>; 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}+
−
  \<open>@{ML_response "1+2" "3"}\<close>\\+
−
  \<open>@{ML_response "(1+2,3)" "(3,\<dots>)"}\<close>+
−
  \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$] \<open>@{ML_response_fake "expr" "pat"}\<close> works just+
−
  like the antiquotation \<open>@{ML_response "expr" "pat"}\<close> 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}+
−
  \<open>@{ML_response_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\+
−
                               & \<open>"a + b = c"}\<close>\smallskip\\ +
−
  \<open>@{ML_response_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\ +
−
                               & \<open>"Exception FAIL raised"}\<close>+
−
  \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$] \<open>@{ML_response_fake_both "expr" "pat"}\<close> 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}+
−
  \<open>@{ML_response_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\+
−
                                    & \<open>"Type unification failed \<dots>"}\<close>+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \item[$\bullet$] \<open>@{ML_file "name"}\<close> 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 \<open>[display]\<close> and +
−
  \<open>[quotes]\<close>. For example+
−
+
−
  \begin{center}\small+
−
  \<open>@{ML [quotes] "\"foo\" ^ \"bar\""}\<close> \;\;produces\;\; @{text [quotes] "foobar"}+
−
  \end{center}+
−
+
−
  whereas+
−
  +
−
  \begin{center}\small+
−
  \<open>@{ML "\"foo\" ^ \"bar\""}\<close> \;\;produces only\;\; \<open>foobar\<close>+
−
  \end{center}+
−
  +
−
  \item Functions and value bindings cannot be defined inside antiquotations; they need+
−
  to be included inside \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>+
−
  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}~\<open>\<verbopen> \<dots> \<verbclose>\<close>+
−
  for ML-code or \isacommand{lemma} \isa{\%linenos} \<open>...\<close> for proofs. The+
−
  tag is \isa{\%linenosgray} when the numbered text should be gray. +
−
+
−
  \end{itemize}+
−
+
−
\<close>+
−
+
−
+
−
+
−
end+
−