simplified EqSubst setup;

obsolete, reuse mk_rews of local simpset;

Toplevel.theory_to_proof;

transactions now always see quasi-functional intermediate checkpoint; removed obsolete theory_theory_to_proof; added

tuned EqSubst setup;

Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;

hide type datatype node; added theory_node, proof_node, is_theory, is_proof, proof_position_of, checkpoint, copy; no_body_context: no history; transaction: test save = true;

tuned print_theorems_theory;

Toplevel.proof_position_of;

store_thm: transfer to current context, i.e. the target theory;

replaced swap by contrapos_np;

added setminus; tuned;

proper handling of simultaneous goals and mutual rules;

provide projections of induct_weak, induct_unsafe;

added strict_mutual_rule;

RuleCases.strict_mutual_rule; export internalize;

changed the name of the type "nOption" to "noption".

added "fresh_singleton" lemma

added more documentation; will now try out a modification of the ok-predicate

Reversed Larry's option/iff change.

substantial additions using locales

exported read|cert_arity interfaces

trace_simp_depth_limit is 1 by default

removed pointless trace msg.

preservation of names

a few more named lemmas

fix: reintroduced pred_ctxt in gen_add_locale

tuned;

* Pure/Isar: Toplevel.theory_theory_to_proof;

added unlocalize_mfix;

added unlocalize_mixfix;

added theory_to_theory_to_proof, which may change theory before entering the proof; added forget_proof (from isar_thy.ML);

tuned;

moved forget_proof to toplevel.ML;

Toplevel.forget_proof;

adapted Toplevel.Proof;

removed dead code;

more stuff;

Provers/classical: stricter checks to ensure that supplied intro, dest and elim rules are well-formed

added explicit paths to required theories

added implementation manual;

more stuff;

fixed LaTeX source;

class now a keyword

class now an keyword, quoted where necessary

add_local_context now yields imported and body elements seperatly; additional slight clenup in code

rearranged burrow_split to fold_burrow to allow composition with fold_map

added unfolding(_i); renamed using_thmss(_i) to using_i;

unparse String/AltString: escape quotes;

tuned;

avoid hardwired Trueprop; local proof: static refererence to Pure.thy;

added 'using' command;

updated;

added IsarImplementation;

updated -- lost update!?

* Pure/Isar: new command 'unfolding'; * ML/Provers: more generic wrt. syntax of object-logics; tuned;

ISABELLE_USER for remote cvs access;

outline;

"The Isabelle/Isar Implementation" manual;

* Provers/classical: removed obsolete classical version of elim_format;