LocalDefs.cert_def; tuned;

eq_prop: Envir.beta_eta_contract;

renamed xxx_multi to xxx_list; tuned;

moved combound, rlist_abs to logic.ML;

union_tpairs: Library.merge; Envir.(beta_)eta_contract; tuned;

moved no_vars to sign.ML; removed dest_def (cf. Sign.cert_def);

lambda: abstract over any const; tuned;

added add_abbrevs(_i); moved const_of_class/class_of_const to logic.ML; added no_vars (from theory.ML); added cert_def; added const_expansion; certify: refer to Consts.certify, which includes expansion;

moved (beta_)eta_contract to envir.ML; tuned;

tuned;

added generic dest_def (mostly from theory.ML); added abs_def (from Isar/local_defs.ML); added const_of_class/class_of_const (from sign.ML); added combound, rlist_abs (from unify.ML);

added (beta_)eta_contract (from pattern.ML); added expand_atom;

print_theory: const abbreviations;

added abbreviations; added certify (mostly from sign.ML);

load envir.ML and logic.ML early;

Logic.rlist_abs;

Logic.const_of_class/class_of_const;

TableFun: renamed xxx_multi to xxx_list;

replaced Symtab.merge_multi by local merge_rules;

Envir.(beta_)eta_contract;

subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate

added strip_abs

clarified semantics of merge

speedup: use simproc for AC rules

UU_reorient_simproc no longer rewrites UU = numeral

removed obsolete gen_ins/mem; added merge -- supercedes gen_merge_lists';

removed add/del_rules;

canonical member/insert/merge;

removal of case analysis clauses

fix

minor improvements

refined signature of locale module

no toplevel 'thy' anymore

fix in codegen

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.

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;

all styles now reset to defaults first, i.e. the document may switch styles back and forth; added macro \isachardefaults for \chardef defaults; renamed \isakeywordcharunderscore to \isacharunderscorekeyword; added isabellestyle{default};

export meta_rewrite_rule; tuned;

advanced translations: Context.generic; tuned;

advanced translations: Context.generic;

tidy-up of res_clause.ML, removing the "predicates" field

'setup': no list type, support implicit setup; tuned;

'fixes': support plain vars; classical attributes: optional weight -- ignored by automated tools;

fixed a syntax error!

replaced gen_list by enum

adaptions to codegen_package

various improvements

added three times overloaded Isar instance command

moved instance Isar command to class_package.ML

added map_atype, map_aterms

tuned proof;

declare atomize/defn for Ball;

invent_fixes: merely enter body temporarily;

'unfolding': LocalDefs.unfold;

moved treatment of object-logic equalities to local_defs.ML;

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

added attributes defn_add/del; added (un)fold operations (from object_logic.ML); tuned;

added 'defn' attribute; attribute (un)folded: option '(raw)';

proper order of trfuns;

CPure: Context.add_setup;