--- a/doc-src/IsarImplementation/Thy/ML.thy Fri Oct 08 21:11:56 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Fri Oct 08 21:49:16 2010 +0100
@@ -171,17 +171,19 @@
subsection {* Antiquotations \label{sec:ML-antiq} *}
text {* A very important consequence of embedding SML into Isar is the
- concept of \emph{ML antiquotation}: the standard token language of
- ML is augmented by special syntactic entities of the following form:
+ concept of \emph{ML antiquotation}. First, the standard token
+ language of ML is augmented by special syntactic entities of the
+ following form:
+ \indexouternonterm{antiquote}
\begin{rail}
antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym
;
\end{rail}
- \noindent Here the syntax categories @{syntax nameref} and @{syntax
- args} are defined in \cite{isabelle-isar-ref}; attributes and proof
- methods use similar syntax.
+ \noindent Here @{syntax nameref} and @{syntax args} are regular
+ outer syntax categories. Note that attributes and proof methods use
+ similar syntax.
\medskip A regular antiquotation @{text "@{name args}"} processes
its arguments by the usual means of the Isar source language, and
@@ -197,6 +199,59 @@
non-ASCII braces @{text "\<lbrace>"} and @{text "\<rbrace>"} allow to delimit the
effect by introducing local blocks within the pre-compilation
environment.
+
+ \bigskip See also \cite{Wenzel-Chaieb:2007b} for a slightly broader
+ perspective on Isabelle/ML antiquotations.
+*}
+
+text %mlref {*
+ \begin{matharray}{rcl}
+ @{ML_antiquotation_def "let"} & : & @{text ML_antiquotation} \\
+ @{ML_antiquotation_def "note"} & : & @{text ML_antiquotation} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'let' ((term + 'and') '=' term + 'and')
+ ;
+
+ 'note' (thmdef? thmrefs + 'and')
+ ;
+ \end{rail}
+
+ \begin{description}
+
+ \item @{text "@{let p = t}"} binds schematic variables in the
+ pattern @{text "p"} by higher-order matching against the term @{text
+ "t"}. This is analogous to the regular @{command_ref let} command
+ in the Isar proof language. The pre-compilation environment is
+ augmented by auxiliary term bindings, without emitting ML source.
+
+ \item @{text "@{note a = b\<^sub>1 \<dots> b\<^sub>n}"} recalls existing facts @{text
+ "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. This is analogous to
+ the regular @{command_ref note} command in the Isar proof language.
+ The pre-compilation environment is augmented by auxiliary fact
+ bindings, without emitting ML source.
+
+ \end{description}
+*}
+
+text %mlex {* The following artificial example gives a first
+ impression about using the antiquotation elements introduced so far,
+ together with the basic @{text "@{thm}"} antiquotation defined
+ later.
+*}
+
+ML {*
+ \<lbrace>
+ @{let ?t = my_term}
+ @{note my_refl = reflexive [of ?t]}
+ fun foo th = Thm.transitive th @{thm my_refl}
+ \<rbrace>
+*}
+
+text {*
+ The extra block delimiters do not affect the compiled code itself, i.e.\
+ function @{ML foo} is available in the present context.
*}
end
\ No newline at end of file
--- a/doc-src/antiquote_setup.ML Fri Oct 08 21:11:56 2010 +0100
+++ b/doc-src/antiquote_setup.ML Fri Oct 08 21:49:16 2010 +0100
@@ -184,6 +184,7 @@
val _ = entity_antiqs (K check_tool) "isatt" "tool";
val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
+val _ = entity_antiqs no_check "" "ML antiquotation"; (* FIXME proper check *)
end;
--- a/doc-src/manual.bib Fri Oct 08 21:11:56 2010 +0100
+++ b/doc-src/manual.bib Fri Oct 08 21:49:16 2010 +0100
@@ -1569,6 +1569,16 @@
note = {\url{http://www.in.tum.de/~wenzelm/papers/isar-framework.pdf}}
}
+@InProceedings{Wenzel-Chaieb:2007b,
+ author = {Makarius Wenzel and Amine Chaieb},
+ title = {{SML} with antiquotations embedded into {Isabelle/Isar}},
+ booktitle = {Workshop on Programming Languages for Mechanized Mathematics
+ (satellite of CALCULEMUS 2007). Hagenberg, Austria},
+ editor = {Jacques Carette and Freek Wiedijk},
+ month = {June},
+ year = {2007}
+}
+
@book{principia,
author = {A. N. Whitehead and B. Russell},
title = {Principia Mathematica},