Victor Dumitrescu

2016-07-24 09:40:53 UTC

I am struggling with printing the full output of ML code in Isabelle/jEdit.

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.

Also, when using Thm.proof_body_of, for example, the output seems to be

elided in many places (output in Isabelle/jEdit attached below). Is

there a way to retrieve the full output of the function?

Victor Dumitrescu

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.

Also, when using Thm.proof_body_of, for example, the output seems to be

elided in many places (output in Isabelle/jEdit attached below). Is

there a way to retrieve the full output of the function?

PBody {oracles = [], proof =

PThm (1062004,

(("Tree.invert_inv", Const ("HOL.Trueprop",

"bool ⇒ prop") $ (Const ("...", "(tree ⇒ bool) ⇒ bool") $ ...), NONE),

PBody {oracles = [], proof = MinProof, thms =

[(1062003, ("", ... $ ..., PBody

{oracles = [...], ...})), (284, ("...", ..., ...)), (280, ("...",

...))]})),

thms = [(1062004,

("Tree.invert_inv",

Const ("HOL.Trueprop", "bool ⇒ prop") $

(Const ("HOL.All", "(tree ⇒ bool) ⇒ bool") $ Abs ("p", "tree", ...)),

PBody {oracles = [], proof = MinProof, thms =

[(1062003, ("", Const ("...", "bool ⇒

prop") $ ..., PBody {oracles = [...], proof = ..., thms = [...]})),

(284, ("Pure.protectD", ... $ ... $

..., PBody {oracles = [...], ...})), (280, ("...", ..., ...))]}))]}

Thank you,PThm (1062004,

(("Tree.invert_inv", Const ("HOL.Trueprop",

"bool ⇒ prop") $ (Const ("...", "(tree ⇒ bool) ⇒ bool") $ ...), NONE),

PBody {oracles = [], proof = MinProof, thms =

[(1062003, ("", ... $ ..., PBody

{oracles = [...], ...})), (284, ("...", ..., ...)), (280, ("...",

...))]})),

thms = [(1062004,

("Tree.invert_inv",

Const ("HOL.Trueprop", "bool ⇒ prop") $

(Const ("HOL.All", "(tree ⇒ bool) ⇒ bool") $ Abs ("p", "tree", ...)),

PBody {oracles = [], proof = MinProof, thms =

[(1062003, ("", Const ("...", "bool ⇒

prop") $ ..., PBody {oracles = [...], proof = ..., thms = [...]})),

(284, ("Pure.protectD", ... $ ... $

..., PBody {oracles = [...], ...})), (280, ("...", ..., ...))]}))]}

Victor Dumitrescu

--

The University of Edinburgh is a charitable body, registered in

Scotland, with registration number SC005336.

The University of Edinburgh is a charitable body, registered in

Scotland, with registration number SC005336.