--- a/ProgTutorial/Appendix.thy	Tue Oct 20 12:25:20 2009 +0200
+++ b/ProgTutorial/Appendix.thy	Thu Oct 22 02:03:14 2009 +0200
@@ -29,6 +29,8 @@
   (@{ML_file "Pure/pattern.ML"} implements HOPU)
 
   \item useful datastructures: discrimination nets, association lists
+
+  \item Brief history of Isabelle
   \end{itemize}
 *}
 

--- a/ProgTutorial/General.thy	Tue Oct 20 12:25:20 2009 +0200
+++ b/ProgTutorial/General.thy	Thu Oct 22 02:03:14 2009 +0200
@@ -714,10 +714,11 @@
 "let
   val natT = @{typ \"nat\"}
   val zero = @{term \"0::nat\"}
+  val plus = Const (@{const_name plus}, [natT, natT] ---> natT)
 in
-  cterm_of @{theory} 
-      (Const (@{const_name plus}, [natT, natT] ---> natT) $ zero $ zero)
-end" "0 + 0"}
+  cterm_of @{theory} (plus $ zero $ zero)
+end" 
+  "0 + 0"}
 
   In Isabelle not just terms need to be certified, but also types. For example, 
   you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on 
@@ -899,8 +900,7 @@
   (type T = thm list
    val empty = []
    val extend = I
-   val merge = K (op @) 
-)
+   val merge = K (op @))
 
 fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*}
 
@@ -1254,8 +1254,7 @@
   We can now install a the modified theorem style as follows
 *}
 
-setup %gray {*
-let
+setup %gray {* let
   val parser = Scan.repeat Args.name
   fun action xs = K (rename_allq xs #> strip_allq)
 in
@@ -1288,8 +1287,8 @@
 text {*
   Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
   "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
-  annotated to theorems, but functions that do further processing once a
-  theorem is proved. In particular, it is not possible to find out
+  annotated to theorems, but functions that do further processing of 
+  theorems. In particular, it is not possible to find out
   what are all theorems that have a given attribute in common, unless of course
   the function behind the attribute stores the theorems in a retrievable 
   data structure. 
@@ -1306,9 +1305,9 @@
   \end{isabelle}
   
   The theorem attributes fall roughly into two categories: the first category manipulates
-  the proved theorem (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
-  stores the proved theorem somewhere as data (for example @{text "[simp]"}, which adds
-  the theorem to the current simpset).
+  theorems (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
+  stores theorems somewhere as data (for example @{text "[simp]"}, which adds
+  theorems to the current simpset).
 
   To explain how to write your own attribute, let us start with an extremely simple 
   version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
@@ -1330,15 +1329,14 @@
   using the Isabelle command \isacommand{attribute\_setup} as follows:
 *}
 
-attribute_setup %gray my_sym = {* Scan.succeed my_symmetric *} 
-  "applying the sym rule"
+attribute_setup %gray my_sym = 
+  {* Scan.succeed my_symmetric *} "applying the sym rule"
 
 text {*
   Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser
   for the theorem attribute. Since the attribute does not expect any further 
-  arguments (unlike @{text "[THEN \<dots>]"}, for example), we use the parser @{ML
-  Scan.succeed}. Later on we will also consider attributes taking further
-  arguments. An example for the attribute @{text "[my_sym]"} is the proof
+  arguments (unlike @{text "[THEN \<dots>]"}, for instance), we use the parser @{ML
+  Scan.succeed}. An example for the attribute @{text "[my_sym]"} is the proof
 *} 
 
 lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
@@ -1368,17 +1366,17 @@
   "applying the sym rule" *}
 
 text {*
-  This gives a function from @{ML_type "Context.theory -> Context.theory"}, which
+  This gives a function from @{ML_type "theory -> theory"}, which
   can be used for example with \isacommand{setup}.
 
   As an example of a slightly more complicated theorem attribute, we implement 
   our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
-  as argument and resolve the proved theorem with this list (one theorem 
+  as argument and resolve the theorem with this list (one theorem 
   after another). The code for this attribute is
 *}
 
 ML{*fun MY_THEN thms = 
-  Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}
+  Thm.rule_attribute (fn _ => fn thm => List.foldl ((op RS) o swap) thm thms)*}
 
 text {* 
   where @{ML swap} swaps the components of a pair. The setup of this theorem
@@ -1387,7 +1385,7 @@
 *}
 
 attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *} 
-  "resolving the list of theorems with the proved theorem"
+  "resolving the list of theorems with the theorem"
 
 text {* 
   You can, for example, use this theorem attribute to turn an equation into a 
@@ -1863,7 +1861,7 @@
 a
 b"}
   
-  \footnote{\bf What happens with printing big formulae?}
+  \footnote{\bf FIXME: What happens with printing big formulae?}
 
   
 

--- a/ProgTutorial/Intro.thy	Tue Oct 20 12:25:20 2009 +0200
+++ b/ProgTutorial/Intro.thy	Thu Oct 22 02:03:14 2009 +0200
@@ -26,14 +26,20 @@
   If your next project requires you to program on the ML-level of Isabelle,
   then this tutorial is for you. It will guide you through the first steps of
   Isabelle programming, and also explain tricks of the trade. We also hope
-  the tutorial will encourage researchers to play with Isabelle. The best way to
-  get to know the ML-level of Isabelle is by experimenting with the many code
-  examples included in the tutorial. The code is as far as possible checked
-  against the Isabelle distribution.\footnote{\input{version}} If something does not work, 
-  then please let us know. It is impossible for us to know every environment, 
-  operating system or editor in which Isabelle is used. If you have comments, 
-  criticism or like to add to the tutorial, please feel free---you are most 
-  welcome! The tutorial is meant to be gentle and comprehensive. To achieve 
+  the tutorial will encourage researchers to play with Isabelle and implement
+  new ideas. The sources of Isabelle can look intimidating, but beginners 
+  can get by with knowledge of only a small number functions and a few basic
+  coding conventions.
+
+
+  The best way to get to know the ML-level of Isabelle is by experimenting
+  with the many code examples included in the tutorial. The code is as far as
+  possible checked against the Isabelle
+  distribution.\footnote{\input{version}} If something does not work, then
+  please let us know. It is impossible for us to know every environment,
+  operating system or editor in which Isabelle is used. If you have comments,
+  criticism or like to add to the tutorial, please feel free---you are most
+  welcome! The tutorial is meant to be gentle and comprehensive. To achieve
   this we need your feedback.
 *}
 

--- a/ProgTutorial/antiquote_setup.ML	Tue Oct 20 12:25:20 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Thu Oct 22 02:03:14 2009 +0200
@@ -81,13 +81,13 @@
 (* checks and expression agains a result pattern *)
 fun output_response {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_pat (lhs, pat));
-     write_file_ml_blk lhs (Context.theory_of_proof ctxt);
+     write_file_ml_blk lhs (ProofContext.theory_of ctxt);
      output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun output_response_fake {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_val [] NONE lhs);
-     write_file_ml_blk lhs (Context.theory_of_proof ctxt);
+     write_file_ml_blk lhs (ProofContext.theory_of ctxt);
      output ((split_lines lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)

Binary file progtutorial.pdf has changed