tuned comments;

tuned proofs: avoid implicit prems;

clean up instance proofs; reorganize section headings

reactivated theory Class;

added the Q_Unit rule (was missing) and adjusted the proof accordingly

* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account; * Isar: implicit use of prems from the Isar proof context is considered a legacy feature;

generate_fresh works even if there is no free variable in the goal

tuned;

tuned proofs: avoid implicit prems;

removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int

thm antiquotations

transaction: context_position (non-destructive only);

added map_current; simplified internal type proof;

tuned msg;

apply_method/end_proof: pass position; Method.Basic: include position;

renamed map to map_current;

tuned;

removed unused is_atomic;

renamed prove_raw to prove_internal; tuned;

merge/merge_refs: plain error instead of exception TERM;

Context positions.

added context_position.ML;

renamed Goal.prove_raw to Goal.prove_internal;

Method.Basic: include position;

tuned proofs: avoid implicit prems;

Basic text: include position; assumption/close: refer to non-atomic assumptions as well, implicit use of prems now considered legacy feature;

thm antiquotations

add lemma inj_of_nat

thm antiquotations

Unfortunately needed patch due to incompatibility with SML -- oo is infix and hence can not appear on the left handside of patterns

changed int stuff into integer for SMLNJ compatibility

more of_rat lemmas