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

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

> On Fri, 26 Aug 2011, Steve Wong wrote:
> Syntax.string_of_term turns internal formal entities (terms) into external
> text representation for user-consumption.  For historic reasons the string
> type is used here, but it is in fact some kind of quasi-abstract datatype
> for marked-up document content.  In general it is not allowed either to
> split text input that is passed in or paste together text that is passed out
> of the formal environment.
> 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.  (Sometines people forget to provide them, but for
> almost everything in the regular Isabelle distribution there is such a
> proper non-text version, taking directly typ and term values etc.)
> Anyway, instead of Specification.theorem it is probably easier to use
> Proof.theorem, although you need to store the result yourself in the
> "after_qed" continuation.
Thanks a lot for that. 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?

Thanks again.


>        Makarius

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