2006-02-06 wenzelm 2006-02-06 moved (beta_)eta_contract to envir.ML; tuned;
2006-02-06 wenzelm 2006-02-06 tuned;
2006-02-06 wenzelm 2006-02-06 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);
2006-02-06 wenzelm 2006-02-06 added (beta_)eta_contract (from pattern.ML); added expand_atom;
2006-02-06 wenzelm 2006-02-06 print_theory: const abbreviations;
2006-02-06 wenzelm 2006-02-06 added abbreviations; added certify (mostly from sign.ML);
2006-02-06 wenzelm 2006-02-06 load envir.ML and logic.ML early;
2006-02-06 wenzelm 2006-02-06 Logic.rlist_abs;
2006-02-06 wenzelm 2006-02-06 Logic.const_of_class/class_of_const;
2006-02-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list;
2006-02-06 wenzelm 2006-02-06 replaced Symtab.merge_multi by local merge_rules;
2006-02-06 wenzelm 2006-02-06 Envir.(beta_)eta_contract;
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-02-06 haftmann 2006-02-06 added strip_abs
2006-02-06 haftmann 2006-02-06 clarified semantics of merge
2006-02-04 huffman 2006-02-04 speedup: use simproc for AC rules
2006-02-04 huffman 2006-02-04 UU_reorient_simproc no longer rewrites UU = numeral
2006-02-03 wenzelm 2006-02-03 removed obsolete gen_ins/mem; added merge -- supercedes gen_merge_lists';
2006-02-03 wenzelm 2006-02-03 removed add/del_rules;
2006-02-03 wenzelm 2006-02-03 canonical member/insert/merge;
2006-02-03 paulson 2006-02-03 removal of case analysis clauses
2006-02-03 haftmann 2006-02-03 fix
2006-02-03 haftmann 2006-02-03 minor improvements
2006-02-03 haftmann 2006-02-03 refined signature of locale module
2006-02-03 haftmann 2006-02-03 no toplevel 'thy' anymore
2006-02-03 haftmann 2006-02-03 fix in codegen
2006-02-02 wenzelm 2006-02-02 do not open structure;
2006-02-02 huffman 2006-02-02 reimplemented using Equiv_Relations.thy
2006-02-02 haftmann 2006-02-02 improvement in devarifications
2006-02-02 haftmann 2006-02-02 alternative syntax for instances
2006-02-02 wenzelm 2006-02-02 tuned;
2006-02-02 wenzelm 2006-02-02 consumes: negative argument relative to total number of prems;
2006-02-02 wenzelm 2006-02-02 added refine_insert;
2006-02-02 wenzelm 2006-02-02 Proof.refine_insert; statements: always use Attrib.src;
2006-02-02 wenzelm 2006-02-02 always use Attrib.src;
2006-02-02 wenzelm 2006-02-02 more generic type for map_specs/facts;
2006-02-02 wenzelm 2006-02-02 'obtains' element;
2006-02-02 wenzelm 2006-02-02 'obtain': optional case name;
2006-02-02 wenzelm 2006-02-02 index elements;
2006-02-02 wenzelm 2006-02-02 * Isar: 'obtains' element;
2006-02-02 wenzelm 2006-02-02 tuned msg;
2006-02-02 wenzelm 2006-02-02 theorem(_in_locale): Element.statement, Obtain.statement;
2006-02-02 wenzelm 2006-02-02 added parname; added (general_)statement (from isar_syn.ML); general_statement: Elements.statement, i.e. Shows/Obtains;
2006-02-02 wenzelm 2006-02-02 obtain(_i): optional name for 'that'; added statement (cf. Locale.theorem);
2006-02-02 wenzelm 2006-02-02 tuned comments;
2006-02-02 wenzelm 2006-02-02 moved (general_)statement to outer_parse.ML;
2006-02-02 wenzelm 2006-02-02 added concluding statements: Shows/Obtains;
2006-02-02 wenzelm 2006-02-02 moved specific map_typ/term to sign.ML;
2006-02-02 wenzelm 2006-02-02 added specific map_typ/term (from term.ML);
2006-02-02 krauss 2006-02-02 Exporting recdef's hints for use by new recdef package
2006-02-02 ballarin 2006-02-02 *_asms_of fixed.
2006-02-02 kleing 2006-02-02 add 64bit atbroy98 platform
2006-02-01 wenzelm 2006-02-01 updated;
2006-02-01 berghofe 2006-02-01 Added "evaluation" method and oracle.
2006-02-01 paulson 2006-02-01 new and updated protocol proofs by Giamp Bella
2006-02-01 haftmann 2006-02-01 substantial cleanup and simplifications
2006-02-01 haftmann 2006-02-01 name clarifications
2006-02-01 haftmann 2006-02-01 added map_entry_yield
2006-02-01 urbanc 2006-02-01 - renamed some lemmas (some had names coming from ancient versions of the nominal work) - some tuning - eventually this theory should be renamed to CR
2006-02-01 urbanc 2006-02-01 added all constructors from PhD