2006-02-03 ago wenzelm canonical member/insert/merge;
2006-02-03 ago paulson removal of case analysis clauses
2006-02-03 ago haftmann fix
2006-02-03 ago haftmann minor improvements
2006-02-03 ago haftmann refined signature of locale module
2006-02-03 ago haftmann no toplevel 'thy' anymore
2006-02-03 ago haftmann fix in codegen
2006-02-02 ago wenzelm do not open structure;
2006-02-02 ago huffman reimplemented using Equiv_Relations.thy
2006-02-02 ago haftmann improvement in devarifications
2006-02-02 ago haftmann alternative syntax for instances
2006-02-02 ago wenzelm tuned;
2006-02-02 ago wenzelm consumes: negative argument relative to total number of prems;
2006-02-02 ago wenzelm added refine_insert;
2006-02-02 ago wenzelm Proof.refine_insert;
2006-02-02 ago wenzelm always use Attrib.src;
2006-02-02 ago wenzelm more generic type for map_specs/facts;
2006-02-02 ago wenzelm 'obtains' element;
2006-02-02 ago wenzelm 'obtain': optional case name;
2006-02-02 ago wenzelm index elements;
2006-02-02 ago wenzelm * Isar: 'obtains' element;
2006-02-02 ago wenzelm tuned msg;
2006-02-02 ago wenzelm theorem(_in_locale): Element.statement, Obtain.statement;
2006-02-02 ago wenzelm added parname;
2006-02-02 ago wenzelm obtain(_i): optional name for 'that';
2006-02-02 ago wenzelm tuned comments;
2006-02-02 ago wenzelm moved (general_)statement to outer_parse.ML;
2006-02-02 ago wenzelm added concluding statements: Shows/Obtains;
2006-02-02 ago wenzelm moved specific map_typ/term to sign.ML;
2006-02-02 ago wenzelm added specific map_typ/term (from term.ML);
2006-02-02 ago krauss Exporting recdef's hints for use by new recdef package
2006-02-02 ago ballarin *_asms_of fixed.
2006-02-02 ago kleing add 64bit atbroy98 platform
2006-02-01 ago wenzelm updated;
2006-02-01 ago berghofe Added "evaluation" method and oracle.
2006-02-01 ago paulson new and updated protocol proofs by Giamp Bella
2006-02-01 ago haftmann substantial cleanup and simplifications
2006-02-01 ago haftmann name clarifications
2006-02-01 ago haftmann added map_entry_yield
2006-02-01 ago urbanc - renamed some lemmas (some had names coming from ancient
2006-02-01 ago urbanc added all constructors from PhD
2006-01-31 ago wenzelm axiomatization: retrict parameters to occurrences in specs;
2006-01-31 ago wenzelm improved comments;
2006-01-31 ago wenzelm tuned LocalDefs.unfold;
2006-01-31 ago wenzelm (un)fold: removed '(raw)' option;
2006-01-31 ago wenzelm added consts_retricted;
2006-01-31 ago wenzelm (un)fold: no raw flag;
2006-01-31 ago wenzelm tuned;
2006-01-31 ago wenzelm tuned LocalTheory.pretty_consts;
2006-01-31 ago wenzelm (un)folded: removed '(raw)' option;
2006-01-31 ago wenzelm lambda: abstract over TYPE argument, too;
2006-01-31 ago wenzelm tuned comments;
2006-01-31 ago paulson removal of ResClause.num_of_clauses and other simplifications
2006-01-31 ago paulson working SPASS support; much tidying
2006-01-31 ago haftmann added serialization for arbitrary
2006-01-31 ago haftmann minor change to CodegenPackage interface
2006-01-31 ago haftmann minor cleanups
2006-01-31 ago haftmann more coherent lookup extraction functions
2006-01-31 ago paulson reorganization of code to support DFG otuput
2006-01-31 ago wenzelm * Pure: 'advanced' translation functions use Context.generic instead of just theory;