--- 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?}