prefix for equations in primrec specifications

postprocessing of equality

parser: use plain explode, not Symbol.explode!

removed obsolete add_axiomss(_i);

renamed XML.parse_comment_whspc to XML.parse_comments;

renamed parse_comment_whspc to parse_comments; major parser cleanup -- removed junk comments;

removed yxmlN for now; moved test_markup to proof_general_emacs.ML; use efficient YXML markup internally (output, markup, message); message: issue MALFORMED MESSAGE explicitly; tuned;

moved test_markup here;

further cleanup of XML signature;

tuned comments;

further cleanup of XML signature; replaced plain_content by incremental add_content; added stream output;

output: canonical argument order (as opposed to write);

XML.string_of;

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;