equal
deleted
inserted
replaced
255 |
255 |
256 text {* |
256 text {* |
257 Now let us come back to the point about printing terms. |
257 Now let us come back to the point about printing terms. |
258 *} |
258 *} |
259 |
259 |
|
260 ML {* |
|
261 let |
|
262 val trm = @{term "x y z w"} |
|
263 in |
|
264 pwriteln (Pretty.chunks |
|
265 [ pretty_term ctxt0 trm, |
|
266 pretty_term ctxt1 trm, |
|
267 pretty_term ctxt2 trm ]) |
|
268 end |
|
269 *} |
|
270 |
|
271 |
|
272 text {* |
|
273 |
|
274 *} |
|
275 |
260 |
276 |
261 (* |
277 (* |
262 ML{*Proof_Context.debug := true*} |
278 ML{*Proof_Context.debug := true*} |
263 ML{*Proof_Context.verbose := true*} |
279 ML{*Proof_Context.verbose := true*} |
264 *) |
280 *) |