--- a/ProgTutorial/FirstSteps.thy	Mon Sep 28 01:21:27 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Mon Sep 28 23:52:06 2009 +0200
@@ -11,12 +11,13 @@
   ``We will most likely never realize the full importance of painting the Tower,\\ 
   that it is the essential element in the conservation of metal works and the\\ 
   more meticulous the paint job, the longer the Tower shall endure.''} \\[1ex]
-  Gustave Eiffel, In The 300-Meter Tower.\footnote{The Eiffel Tower has been 
+  Gustave Eiffel, In his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 
   re-painted 18 times since its initial construction, an average of once every 
   seven years. It takes more than a year for a team of 25 painters to paint the Tower 
-  from top to bottom.}\\[1ex]
+  from top to bottom.}
   \end{flushright}
 
+  \medskip
   Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
   Isabelle must be part of a theory. If you want to follow the code given in
   this chapter, we assume you are working inside the theory starting with
@@ -30,8 +31,8 @@
   \end{tabular}
   \end{quote}
 
-  We also generally assume you are working with HOL. The given examples might
-  need to be adapted if you work in a different logic.
+  We also generally assume you are working with the logic HOL. The examples
+  that will be given might need to be adapted if you work in a different logic.
 *}
 
 section {* Including ML-Code *}
@@ -252,9 +253,9 @@
   string_of_term ctxt (term_of ct)*}
 
 text {*
-  In this example the function @{ML_ind  term_of} extracts the @{ML_type
+  In this example the function @{ML_ind term_of} extracts the @{ML_type
   term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can again be
-  printed with @{ML_ind  commas}.
+  printed with @{ML_ind commas}.
 *} 
 
 ML{*fun string_of_cterms ctxt cts =  
@@ -262,11 +263,13 @@
 
 text {*
   The easiest way to get the string of a theorem is to transform it
-  into a @{ML_type cterm} using the function @{ML_ind  crep_thm}. 
+  into a @{ML_type term} using the function @{ML_ind prop_of}. 
 *}
 
+ML {* Thm.rep_thm @{thm mp} *}
+
 ML{*fun string_of_thm ctxt thm =
-  string_of_cterm ctxt (#prop (crep_thm thm))*}
+  Syntax.string_of_term ctxt (prop_of thm)*}
 
 text {*
   Theorems also include schematic variables, such as @{text "?P"}, 
@@ -293,7 +296,7 @@
 end
 
 fun string_of_thm_no_vars ctxt thm =
-  string_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
+  Syntax.string_of_term ctxt (prop_of (no_vars ctxt thm))*}
 
 text {* 
   Theorem @{thm [source] conjI} is now printed as follows:
@@ -315,7 +318,7 @@
   Note, that when printing out several parcels of information that
   semantically belong together, like a warning message consisting for example
   of a term and a type, you should try to keep this information together in a
-  single string. So do not print out information as
+  single string. Therefore do not print out information as
 
 @{ML_response_fake [display,gray]
 "tracing \"First half,\"; 
@@ -397,7 +400,7 @@
 text {* or *}
 
 ML{*fun inc_by_five x = 
-       ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
+  ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
 
 text {* and typographically more economical than *}
 
@@ -444,7 +447,7 @@
 
   You can read off this behaviour from how @{ML apply_fresh_args} is
   coded: in Line 2, the function @{ML_ind  fastype_of} calculates the type of the
-  term; @{ML_ind  binder_types} in the next line produces the list of argument
+  term; @{ML_ind binder_types} in the next line produces the list of argument
   types (in the case above the list @{text "[nat, int, unit]"}); Line 4 
   pairs up each type with the string  @{text "z"}; the
   function @{ML_ind  variant_frees in Variable} generates for each @{text "z"} a
@@ -643,21 +646,21 @@
   "let
   val ctxt = @{context}
 in
-  map (Syntax.parse_term ctxt) [\"m + n\", \"m - (n::nat)\"] 
+  map (Syntax.parse_term ctxt) [\"m + n\", \"m * n\", \"m - (n::nat)\"] 
   |> Syntax.check_terms ctxt
   |> string_of_terms ctxt
   |> tracing
 end"
-  "m + n, m - n"}
+  "m + n, m * n, m - n"}
 *}
 
 text {*
-  In this example we obtain two terms with appropriate typing. However, if you
-  have only a single term, then @{ML check_terms in Syntax} needs to be
-  adapted. This can be done with the ``plumbing'' function @{ML
-  singleton}.\footnote{There is already a function @{ML check_term in Syntax}
-  in the Isabelle sources that is defined in terms of @{ML singleton} and @{ML
-  check_terms in Syntax}.} For example
+  In this example we obtain three terms where @{text m} and @{text n} are of
+  type @{typ "nat"}. However, if you have only a single term, then @{ML
+  check_terms in Syntax} needs plumbing. This can be done with the function
+  @{ML singleton}.\footnote{There is already a function @{ML check_term in
+  Syntax} in the Isabelle sources that is defined in terms of @{ML singleton}
+  and @{ML check_terms in Syntax}.} For example
 
   @{ML_response_fake [display, gray]
   "let 
@@ -689,20 +692,18 @@
   The main advantage of embedding all code in a theory is that the code can
   contain references to entities defined on the logical level of Isabelle. By
   this we mean definitions, theorems, terms and so on. This kind of reference
-  is realised with ML-antiquotations, often also referred to as just
+  is realised with ML-antiquotations, often just called
   antiquotations.\footnote{There are two kinds of antiquotations in Isabelle,
   which have very different purpose and infrastructures. The first kind,
   described in this section, are \emph{ML-antiquotations}. They are used to
   refer to entities (like terms, types etc) from Isabelle's logic layer inside
-  ML-code. The other kind of antiquotations are \emph{document} antiquotations. They
-  are used only in the text parts of Isabelle and their purpose is to print
-  logical entities inside \LaTeX-documents. They are part of the user level
-  and therefore we are not interested in them in this Tutorial, except in
-  Appendix \ref{rec:docantiquotations} where we show how to implement your own
-  document antiquotations.}
-  For example, one can print out the name of the current
-  theory by typing
-
+  ML-code. The other kind of antiquotations are \emph{document}
+  antiquotations. They are used only in the text parts of Isabelle and their
+  purpose is to print logical entities inside \LaTeX-documents. They are part
+  of the user level and therefore we are not interested in them in this
+  Tutorial, except in Appendix \ref{rec:docantiquotations} where we show how
+  to implement your own document antiquotations.}  For example, one can print
+  out the name of the current theory by typing
   
   @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
  
@@ -821,11 +822,11 @@
 
 text {*
   The parser in Line 2 provides us with a context and a string; this string is
-  transformed into a term using the function @{ML_ind  read_term_pattern in
-  ProofContext} (Line 4); the next two lines print the term so that the
-  ML-system can understand them. The function @{ML atomic in ML_Syntax}
-  just encloses the term in parentheses. An example for the usage of this 
-  antiquotation is:
+  transformed into a term using the function @{ML_ind read_term_pattern in
+  ProofContext} (Line 4); the next two lines transform the term into a string
+  so that the ML-system can understand them. The function @{ML_ind atomic in
+  ML_Syntax} just encloses the term in parentheses. An example for the usage
+  of this antiquotation is:
 
   @{ML_response_fake [display,gray]
   "@{term_pat \"Suc (?x::nat)\"}"
@@ -844,7 +845,9 @@
 
 text {*
   Isabelle provides a mechanism to store (and retrieve) arbitrary data. Before we 
-  explain this mechanism. 
+  explain this mechanism, let us digress a bit. Convenitional wisdom is that the 
+  type-system of ML ensures that for example an @{ML_type "'a list"} can only
+  hold elements of type @{ML_type "'a"}.
 *}
 
 ML{*signature UNIVERSAL_TYPE =

--- a/ProgTutorial/Helper/Command/Command.thy	Mon Sep 28 01:21:27 2009 +0200
+++ b/ProgTutorial/Helper/Command/Command.thy	Mon Sep 28 23:52:06 2009 +0200
@@ -42,23 +42,25 @@
 ML {*
 val r = ref (NONE:(unit -> term) option)
 *}
-ML {*
+ML{*
 let
-   fun setup_proof (txt, pos) lthy =
+   fun after_qed thm_name thms lthy =
+        LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
+
+   fun setup_proof (thm_name, (txt, pos)) lthy =
    let
      val trm = ML_Context.evaluate lthy true ("r", r) txt
    in
-       Proof.theorem_i NONE (K I) [[(trm,[])]] lthy
-   end;
+     Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy
+   end
 
-   val setup_proof_parser = OuterParse.ML_source >> setup_proof
-        
-   val kind = OuterKeyword.thy_goal
+   val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
+ 
 in
    OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" 
-    kind setup_proof_parser
-end
-*}
+     OuterKeyword.thy_goal (parser >> setup_proof)
+end*}
+
 
 (*
 ML {*

--- a/ProgTutorial/Intro.thy	Mon Sep 28 01:21:27 2009 +0200
+++ b/ProgTutorial/Intro.thy	Mon Sep 28 23:52:06 2009 +0200
@@ -12,7 +12,7 @@
   pyramid, but at the top. It's creative design of the highest order. It \\
   isn't monkey or donkey work; rather, as Edsger Dijkstra famously \\
   claimed, it's amongst the hardest intellectual tasks ever attempted.''} \\[1ex]
-  Richard Bornat, In Defence of Programming \cite{Bornat-lecture}
+  Richard Bornat, In {\em Defence of Programming}. \cite{Bornat-lecture}
   \end{flushright}
 
   \medskip

--- a/ProgTutorial/Parsing.thy	Mon Sep 28 01:21:27 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Mon Sep 28 23:52:06 2009 +0200
@@ -1070,22 +1070,24 @@
 
 ML_val{*val r = ref (NONE:(unit -> term) option)*}
 ML{*let
-   fun setup_proof (txt, pos) lthy =
+   fun after_qed thm_name thms lthy =
+        LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
+
+   fun setup_proof (thm_name, (txt, pos)) lthy =
    let
      val trm = ML_Context.evaluate lthy true ("r", r) txt
    in
-       Proof.theorem_i NONE (K I) [[(trm,[])]] lthy
-   end;
+     Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy
+   end
 
-   val setup_proof_parser = OuterParse.ML_source >> setup_proof
-        
-   val kind = OuterKeyword.thy_goal
+   val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
+ 
 in
    OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" 
-    kind setup_proof_parser
+     OuterKeyword.thy_goal (parser >> setup_proof)
 end*}
 
-foobar_prove {* @{prop "True"} *}
+foobar_prove test: {* @{prop "True"} *}
 apply(rule TrueI)
 done
 

Binary file progtutorial.pdf has changed