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;

tuned proofs;

implicit setup;

default rule step: norm_hhf_tac;

tuned comment;

declare 'defn' rules;

LocalDefs;

Basic operations on local definitions.

removed unnecessary Syntax.fix_mixfix;

added axiomatization_loc, definition_loc; definition: let LocalDefs.derived_def do the actual work;

moved local defs to local_defs.ML;

LocalDefs; unfolding(_i): support object-level rewrites;

removed unatomize; added versions of meta_rewrite, unfold, fold;

(un)fold: support object-level rewrites;

added print_consts; tuned;

removed obsolete keyword 'files';

(un)folded: support object-level rewrites;

added equals_cong;

added Isar/local_defs.ML;

LocalDefs.add_def;

LocalDefs.def_export;

tuned proofs;

Pure/Isar: (un)folded, (un)fold, unfolding support object-level rewrite rules; ML/Isar: installed ML toplevel pretty printer for type Proof.context;

interrupt_timeout for Poly replaced by stub

added atomize_iff;

renamed Pretty.gen_list to Pretty.enum;

swapped theory_context;

swapped Toplevel.theory_context; definition(_i): actually rulify as well, support more of object-logic; definition(_i): more precise treatment of local fixes;

added invent_fixes; added debug flag, pprint_context;

swapped Toplevel.theory_context; tuned;

renamed reverse_atomize to unatomize; added rulify_term/tac;

init: include view; swapped Toplevel.theory_context; removed obsolete smart_note_thmss; moved note_thmss_qualified to PureThy; unified code of note_thmss(_i), add_thmss, locale_results;

improved 'notes', including proper treatment of locale results; tuned;

swapped Toplevel.theory_context;

Locale.init;

renamed gen_list to enum; added separate; tuned;

moved theorem tags from Drule to PureThy; replaced kind attribute by kind string; tuned name_multi: index > 1 only; added note_thmss_qualified (from Isar/locale.ML);

added ProofContext.pprint_context (depends on ProofContext.debug);

moved theorem tags from Drule to PureThy;

tidying up SPASS output

tidying

better reporting