Mercurial Mercurial > hg > isabelle-cookbook / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned solution with comb_conv
authorChristian Urban <urbanc@in.tum.de>
Tue, 24 Nov 2009 16:34:39 +0100
changeset 402 a64f91de2eab
parent 401 36d61044f9bf
child 403 444bc9f17cfc
tuned solution with comb_conv
ProgTutorial/Solutions.thy file | annotate | diff | comparison | revisions
progtutorial.pdf file | annotate | diff | comparison | revisions 
--- 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)
 
Binary file progtutorial.pdf has changed
isabelle-cookbook