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*}