moved output_markup to xml.ML; added yxmlN mode name;

XML.output_markup;

XML.string_of, XML.parse;

replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.; added output_markup, parse_element; detect: check XY; tuned comments; tuned;

added output_markup (from Tools/isabelle_process.ML); major cleanup of signature;

replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;

tuned comments;

Added skip_mono flag to inductive definition package.

Added skip_mono flag to inductive definition package.

Added skip_mono flag and inductive_flags type.

Deleted code for axiomatic introduction of datatypes. Instead, the package now uses SkipProof.prove rather than Goal.prove to do proofs.

Removed QuickAndDirty constructor from simproc_dist datatype.

- use SkipProof.prove_global instead of Goal.prove_global - added skip_mono flag to inductive definition package

Added prove_global.

Function package no longer overwrites theorems. Some tuning.

Why XML notation?

Symbol.STX, Symbol.DEL;

Symbol.SOH;

added detect; removed auxiliary buffer_of_tree; tuned;

added some ASCII control symbols;

added Pure/General/yxml.ML;

added generalised definitions for freshness of sets of atoms and lists of atoms

tuned imports

tuned

subst_alias

improved improvements for instantiaton

canonical meet_sort operation

removed obscure "attach" feature