read_const: include type;

renamed 'const_syntax' to 'notation'; proper notation for fixed variables;

updated;

Adapted to changes in FixedPoint theory.

method exported

updated NEWS

* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. Richer structures do not inherit from semiring_0 anymore, because anihilation is a theorem there, not an axiom. * Generalized axclass "recpower" to arbitrary monoid, not just commutative semirings.

added gfx

dropped blastdata.ML

(adjustions)

two further lemmas on split

removed dependency of ord on eq

removed itrev as inlining theorem

added state monad to HOL library

code generator module naming improved

(continued)

(continued)

minor cleanup

case_tr: do not intern already internal consts;

updated;

removed isactrlconst;

instantiate: avoid global references;

added const_syntax_name;

removed obsolete first_duplicate;

added syntax_name;

fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;

Sign.const_syntax_name;

added gfx

removed checkpoint interface; moved back to copy/checkpoint instead of checkpoint/checkpoint (NB 1: checkpoint is idempotent, i.e. impure data is being shared, which is inappropriate; NB 2: copying a checkpoint always produces a related theory); present_proof: proper treatment of history; tuned;

String.compare: slow version -- performance test;

replaced apply_copy by apply'; tuned;

removed is_Trueprop (use can dest_Trueprop'' instead);