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;