# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259076879 -3600
# Node ID a64f91de2eabcdb350066f4280d4a449bd9d2c86
# Parent  36d61044f9bf20d580d6dc205d135f447e4a9bc1
tuned solution with comb_conv

diff -r 36d61044f9bf -r a64f91de2eab ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Sun Nov 22 15:27:10 2009 +0100
+++ b/ProgTutorial/Solutions.thy	Tue Nov 24 16:34:39 2009 +0100
@@ -254,8 +254,7 @@
      @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
          (Conv.binop_conv (add_conv ctxt)
           then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm         
-    | _ $ _ => Conv.combination_conv 
-                 (add_conv ctxt) (add_conv ctxt) ctrm
+    | _ $ _ => Conv.comb_conv (add_conv ctxt) ctrm
     | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm
     | _ => Conv.all_conv ctrm)
 
diff -r 36d61044f9bf -r a64f91de2eab progtutorial.pdf
Binary file progtutorial.pdf has changed