uniform handling of fixes; tuned;

tuned;

generic_setup: optional argument, defaults to Context.setup();

added map_theory, map_proof;

removed obsolete sign_of;

implicit setup, which admits exception_trace;

ProofContext.def_export;

updated to new induction principle

cahges to use the new induction-principle (now proved in full glory)

changes to make use of the new induction principle proved by Stefan horay (hooraayyy)

Implemented proof of (strong) induction rule.

Added theorem at_finite_select.

added lemmas perm_empty, perm_insert to do with permutations on sets

merged the silly lemmas into the eqvt proof of subtype

tuned proofs

tuned the eqvt-proof

rolled back the last addition since these lemmas were already in the simpset.

added the thms-collection "pt_id" (collection of all pt_<ak>1 lemmas)

tuned

tidied, and added missing thm divide_less_eq_1_neg

tidied, and giving theorems names

add transitivity rules

tuned;

updated;

tuned;

generic attributes;

* ML: generic context, data, attributes;

added context_of -- generic context;

generic attributes; tuned;

print rules: generic context;

Specification.pretty_consts ctxt;

generic data and attributes; tuned;

added rule, declaration; support generic attributes: theory, context, generic, common, generic_attribute(_i); added generic syntax; basic attributes now generic; tuned;

added generic syntax; mk_attribute: generic;

tuned dependencies;

added declaration_attribute;

support for generic contexts with data;

fix_tac: no warning;

generic attributes; added low-level modifiers from Pure/context_rules.ML;

Attrib.rule;

tuned

added the lemmas supp_char and supp_string

added some lemmas to the collection "abs_fresh" the lemmas are of the form finite (supp x) ==> (b # [a].x) = (b=a \/ b # x) previously only lemmas of the form (b # [a].x) = (b=a \/ b # x) with the type-constraint that x is finitely supported were included.

_E suffix for compatibility with AddIffs

tidied

simplified the special-case simprules

theorems need names

commented the transitivity and narrowing proof

Theory specifications --- with type-inference, but no internal polymorphism.

added infer_type, declared_type;

added param, spec, named_spec;

added init; tuned signature;

added 'axiomatization';

Specification.pretty_consts;

gen_names: preserve empty names;

added Isar/specification.ML;

updated;

another change for the new induct-method

RuleCases.make_nested;

support nested cases; tuned apply_case;

support nested cases; added apply_case; replaced make/simple by make_common/nested/simple;

RuleCases.make_common;

pretty_locale: backquote notes;

RuleCases.make_simple;

tuned order;

added backquote;

RuleCases.make_common/nested;

* Provers/induct: improved simultaneous goals -- nested cases;

added private datatype nprod (copy of prod) to be used in the induction rule

changed PRO_RED proof to conform with the new induction rules

prep_meta_eq: reuse mk_rews of local simpset; adapted ML code to common conventions; tuned;

removed obsolete eqrule_HOL_data.ML;

removed obsolete eqrule_FOL_data.ML;

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