Re: [isabelle] [isabelle-dev] Malformed YXML encoding

On Fri, 26 Aug 2011, Steve Wong wrote:

On Fri, Aug 26, 2011 at 12:26 PM, Makarius <makarius at> wrote:

On Fri, 26 Aug 2011, Steve Wong wrote:

Working with string interfaces for formal entities was never robust, even
20 years ago, but now the fragility has become immediately apparent. When
"generating" things, you should always use the regular non-text versions of
tools and packages.

So, which are the tools recommended for constructing new terms (based on some existing terms)? Are you referring to functions like dest_Free in term.ML, i.e. destruct a term into parts and then create a new term from ground up?

Either using directly the datype constructors of typ/term (e.g. in pattern matching) or some derived functions from src/Pure/term.ML, src/Pure/logic.ML, src/HOL/Tools/hologic.ML.

The "tools and packages" that I mentioned above are more complex things like Function_Fun.add_fun (the regular ML version) instead of the add_fun_cmd as string version for end-users.


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