theory Readme

imports Base

begin

  \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

  \end{tabular}

  \end{center}

  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}

  for displaying any ML-ex\-pression, because the antiquotation checks whether

  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}

  \end{tabular}

  \end{center}

  display ML-expressions and their response.  The first expression is checked

  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}

  \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}).

  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}

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

  used to show erroneous code. Neither the code nor the response will be

  checked. An example is:

  \begin{center}\small

  \begin{tabular}{ll}

  \end{tabular}

  \end{center}

  referring to a file. It checks whether the file exists.  An example

  is 

  @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}

  \end{itemize}

  \begin{center}\small

  \end{center}

  whereas

  \begin{center}\small

  \end{center}

  \item Functions and value bindings cannot be defined inside antiquotations; they need

  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 

  tag is \isa{\%linenosgray} when the numbered text should be gray. 

  \end{itemize}

end