# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1329317523 0
# Node ID 231ec0c45bff25c1ef49a64d53e07303af2654e4
# Parent  386375b7a22abbc3b20429aa93625e34484e8d2c
remerged

diff -r 386375b7a22a -r 231ec0c45bff ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Wed Feb 15 14:47:46 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Wed Feb 15 14:52:03 2012 +0000
@@ -2127,17 +2127,17 @@
   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
     (Const (\"Groups.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
 
-  or in the pretty-printed form
+or in the pretty-printed form
 
   @{ML_response_fake [display,gray]
 "let
-  val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
-  val two = @{cterm \"2::nat\"}
-  val ten = @{cterm \"10::nat\"}
-  val ctrm = Thm.capply (Thm.capply add two) ten
-  val ctxt = @{context}
-    |> Config.put eta_contract false 
-    |> Config.put show_abbrevs false 
+   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+   val two = @{cterm \"2::nat\"}
+   val ten = @{cterm \"10::nat\"}
+   val ctrm = Thm.capply (Thm.capply add two) ten
+   val ctxt = @{context}
+     |> Config.put eta_contract false 
+     |> Config.put show_abbrevs false 
 in
   Thm.prop_of (Thm.beta_conversion true ctrm)
   |> pretty_term ctxt
diff -r 386375b7a22a -r 231ec0c45bff progtutorial.pdf
Binary file progtutorial.pdf has changed