added name_facts;

tuned Isar proof elements;

added cheating, sorry_text (from skip_proofs.ML); added method_setup (from isar_thy.ML);

load late, after proof.ML; added goal commands: theorem, interpretation etc.; tuned some warnings -- single line only;

moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.); begin_theory: tuned interface, check uses in thy_info.ML;

cleanup parsers and interfaces;

Proof.get_thmss;

tuned;

more self-contained proof elements (material from isar_thy.ML); tuned;

added cases, rule_contextN; eliminated obsolete Sign.sg;

load locale.ML late (after proof.ML); tuned module arrangement;

added maps, map_list, lift, lifts;

added stack.ML;

added simple_fact; generalized no_attributes;

Seq.maps;

added hide_names(_i) (from isar_thy.ML);

added generic_setup, add_oracle (from isar_thy.ML);

added exception EXCEPTION of exn * string;

replaced DATA_FAIL by EXCEPTION;

tuned Isar interfaces; tuned IsarThy.theorem_i;

added General/stack.ML, Isar/proof_display.ML;

the_list (cf. Pure/library.ML);

tuned IsarThy.theorem_i;

fixed INST: has same semantic now as INST_TYPE for repetitions

list of constants and theorems whose names have been changed or merged

add header

added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging

updated to work with latest HOL-Complex

add file Hyperreal/transfer.ML

new implementation of transfer principle