do not open structure;

reimplemented using Equiv_Relations.thy

improvement in devarifications

alternative syntax for instances

tuned;

consumes: negative argument relative to total number of prems;

added refine_insert;

Proof.refine_insert; statements: always use Attrib.src;

always use Attrib.src;

more generic type for map_specs/facts;

'obtains' element;

'obtain': optional case name;

index elements;

* Isar: 'obtains' element;

tuned msg;

theorem(_in_locale): Element.statement, Obtain.statement;

added parname; added (general_)statement (from isar_syn.ML); general_statement: Elements.statement, i.e. Shows/Obtains;

obtain(_i): optional name for 'that'; added statement (cf. Locale.theorem);

tuned comments;

moved (general_)statement to outer_parse.ML;

added concluding statements: Shows/Obtains;

moved specific map_typ/term to sign.ML;

added specific map_typ/term (from term.ML);

Exporting recdef's hints for use by new recdef package

*_asms_of fixed.

add 64bit atbroy98 platform

updated;

Added "evaluation" method and oracle.