# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1320941177 0
# Node ID e3656cc81d272cbc736a04ee2c467268a422df2f
# Parent  fc00bb412a65131a63103b754acd3e0300bf87bc
tuned

diff -r fc00bb412a65 -r e3656cc81d27 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Thu Nov 10 15:54:13 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Thu Nov 10 16:06:17 2011 +0000
@@ -257,6 +257,22 @@
   Now let us come back to the point about printing terms.
 *}
 
+ML {*
+let
+  val trm = @{term "x y z w"}
+in
+  pwriteln (Pretty.chunks 
+    [ pretty_term ctxt0 trm,
+      pretty_term ctxt1 trm,
+      pretty_term ctxt2 trm ])
+end
+*}
+
+
+text {*
+  
+*}
+
 
 (*
 ML{*Proof_Context.debug := true*}
diff -r fc00bb412a65 -r e3656cc81d27 progtutorial.pdf
Binary file progtutorial.pdf has changed