changed the representation of atoms to datatypes over nats

ProofContext.mode_abbrev;

removed obsolete set_expand_abbrevs (superceded by mode_abbrev); pretty_term_abbrev: silently ignore ill-typed term; gen_bind: set_mode only locally;

certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;

certify: do_expand as explicit argument, actually certify type of abstractions; tuned signature; tuned;

tuned;

added has_abs (from envir.ML);

Term.has_abs;

proper signature constraint; minor tuning;

added interrupt_timeout; tuned signature;

Generic interpretation of theory data.

tuned signature; moved generic interpretation to interpretation.ML; added abstract at_begin/end wrappers;

avoid Theory.rep_theory;

added interpretation.ML;

improved error behaviour of use (bootstrap version);

more precise treatment of free dictionary parameters for evaluation

fixed cg setup

restored ml system independence

more permissive

clarified code lemmas

fixed wrong syntax treatment in class target

code lemmas for cardinality

- eval_term no longer computes result during compile time - generated ML code is now compiled via ML_Context.use_mltext rather than use_text; this makes sure that antiquotations are expanded - quickcheck now checks whether types to be substituted for type variables have correct sorts; this avoids spurious counterexamples - execution time for auto_quickcheck is now limited

improved computing

changed lemmas

ml_output: proper error instead of error_msg;

comment added to explain a potential scheduling problem

tuned

*** empty log message ***

metis too slow

move at-sml-dev to 2-processor atbroy100

make sun-sml-dev non-proof-term, and at-sml-def -p 2 (at-sml-dev being moved to faster atbroy100)