Re: [isabelle] Isabelle2015-RC0 ML ATP_Util.unyxml

On Mon, 13 Apr 2015, C. Diekmann wrote:

I'm looking for a replacement of the ATP_Util.unyxml ML function. I
was using it the following:

This is now called YXML.content_of.

fun term_to_string (ctx: Proof.context) (n: term) : string =
 n |> Syntax.pretty_term ctx |> Pretty.string_of |> ATP_Util.unyxml

Here is a more canonical version of the above, using standard Isabelle/ML idioms:

ML â
fun term_to_string ctxt t =
  Syntax.pretty_term ctxt t |> Pretty.string_of |> YXML.content_of

Types carry a priori no meaning in ML, especially the main types of the LCF framework. Above Proof.context, term, and also string don't say anything specific about what you give in an get out (the string it is essentially a markup tree). The language is semantically untyped in this respect.

Instead, you use canonical names for what you mean: proper spelling of "ctxt" is especially important. In the "implementation" manual section 0.1.2 there are more hints on professional usage of names in Isabelle/ML.


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