P.locale_element;

added fold_terms; added tfrees_of, frees_of; tvars_intr_list: natural argument order;

added Isar/element.ML;

Thm.varifyT': natural argument order;

added join function

allowing indentation of 'theory' keyword

simplified after_qed;

avoid prove_plain, export_plain, simplified after_qed; witness = term * thm, i.e. the original proposition with a protected fact (this achieves reliable discharge and allows facts to be slightly more general/normalized); internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly; ObjectLogic.ensure_propT;

removed export_plain; (some_)fact_tac: Drule.incr_indexes;

renamed assert_prop to ensure_prop;

renamed goals.ML to old_goals.ML; inline Drule.impose_hyps;

export compose_hhf; removed obsolete norm_hhf_plain; tuned;

removed impose_hyps, satisfy_hyps; tuned;

const args: do not store variable names (unused);

renamed goals.ML to old_goals.ML;

(fix for accidental commit)

(codegen)

generate pattern combinators for new datatypes

reimplemented Case syntax using print/parse translations; moved as-patterns to separate section

add case syntax for type one

remove syntax for as-patterns

avoid 'as' as identifier;

avoid 'as' as identifier;

Added strong induction theorem (currently only axiomatized!).

Initial commit.

Initial commit of the theory "Weakening".

added thms perm, distinct and fresh to the simplifier. One would liket to add also inject, but this causes problems with "congruences" like Lam [a].t1 = Lam [b].t2 P (Lam [a].t1) ----------------------- P (Lam [b].t2) because the equation "Lam [a].t1 = Lam [b].t2" would simplify to "[a].t1 = [b].t2" and then the goal is not true just by simplification.

added proper fillin_mixfix

added fillin_mixfix, replace_quote

New function store_thmss_atts.