--- a/ProgTutorial/Appendix.thy	Wed Dec 02 02:34:09 2009 +0100
+++ b/ProgTutorial/Appendix.thy	Wed Dec 02 03:46:32 2009 +0100
@@ -25,10 +25,7 @@
   
   \item user space type systems (in the form that already exists)
 
-  \item unification and typing algorithms 
-  (@{ML_file "Pure/pattern.ML"} implements HOPU)
-
-  \item useful datastructures: discrimination nets, association lists
+  \item useful datastructures: discrimination nets, graphs, association lists
 
   \item Brief history of Isabelle
   \end{itemize}

--- a/ProgTutorial/Solutions.thy	Wed Dec 02 02:34:09 2009 +0100
+++ b/ProgTutorial/Solutions.thy	Wed Dec 02 03:46:32 2009 +0100
@@ -100,7 +100,9 @@
    || parse_factor) xs*}
 
 
-text {* \solution{ex:dyckhoff} 
+text {* \solution{ex:dyckhoff} *}
+
+text {* 
   The axiom rule can be implemented with the function @{ML atac}. The other
   rules correspond to the theorems:
 
@@ -242,7 +244,7 @@
   exercise.
 *}
 
-ML {*fun add_simple_conv ctxt ctrm =
+ML{*fun add_simple_conv ctxt ctrm =
 let
   val trm = Thm.term_of ctrm
 in
@@ -273,7 +275,7 @@
   \end{minipage}\bigskip
 *}(*<*)oops(*>*)
 
-text {* \solution{ex:addconversion} *}
+text {* \solution{ex:compare} *}
 
 text {* 
   We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.
@@ -327,7 +329,8 @@
         timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})])
 in
   val c_tac = mk_tac (add_tac @{context}) 
-  val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))
+  val s_tac = mk_tac (simp_tac 
+                       (HOL_basic_ss addsimprocs [@{simproc add_sp}]))
 end*}
 
 text {*

Binary file progtutorial.pdf has changed