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