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.

new and updated protocol proofs by Giamp Bella

substantial cleanup and simplifications

name clarifications

added map_entry_yield

- renamed some lemmas (some had names coming from ancient versions of the nominal work) - some tuning - eventually this theory should be renamed to CR

added all constructors from PhD

axiomatization: retrict parameters to occurrences in specs; definition: restrict parameters to individual rhs;

improved comments;

tuned LocalDefs.unfold;

(un)fold: removed '(raw)' option;

added consts_retricted; pretty/print_consts: parameter restriction;

(un)fold: no raw flag; tuned;

tuned;

tuned LocalTheory.pretty_consts;

(un)folded: removed '(raw)' option;

lambda: abstract over TYPE argument, too;

tuned comments;

removal of ResClause.num_of_clauses and other simplifications

working SPASS support; much tidying

added serialization for arbitrary

minor change to CodegenPackage interface

minor cleanups

more coherent lookup extraction functions

reorganization of code to support DFG otuput

* Pure: 'advanced' translation functions use Context.generic instead of just theory;

declare defn rules;