Re: [isabelle] make_string



> And I can get Abs ("x", TFree ("'a", ["HOL.type"]), Bound 0) printed on
> the screen, and by using @{make_string}, coupled with |> YXML.parse_body
> |> XML.content_of I can get it into a string value.

How, if I may ask? If you can get this printed on the screen, surely you
must have it as a string somehow? So why shoving this to @{make_string}
again?




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