Re: [isabelle] Printing full ML output in Isabelle/jEdit



Hi Victor,

> Specifically, I cannot figure out how to print the full contents of a
> list (the default is 10). I have tried increasing PolyML.print_depth,
> with no effect.

as far as I know, the canonical way of setting the print depth is via an
Isar attribute:

  declare [[ML_print_depth=1000]]

Setting this to a sufficiently high value should also solve your problem
below. Beware that proof terms can be very big and pretty printing them
in full will produce a lot of output.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.