src/HOL/Nominal/nominal_thmdecls.ML
2009-04-27 ago tuned
2009-04-26 ago deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
2009-03-15 ago simplified attribute setup;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-02-25 ago Replaced Logic.unvarify by Variable.import_terms to make declaration of
2009-01-21 ago binding replaces bstring
2008-05-17 ago structure Display: less pervasive operations;
2008-04-15 ago proper dynamic facts for eqvts, freshs, bijs;
2008-03-25 ago update_context: always store as "Nominal.eqvts";
2008-03-20 ago simplified get_thm(s): back to plain name argument;
2008-03-19 ago auxiliary dynamic_thm(s) for fact lookup;
2007-09-13 ago some cleaning up to do with contexts
2007-08-14 ago avoid low-level tsig;
2007-08-14 ago fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
2007-07-29 ago renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-05-07 ago simplified DataFun interfaces;
2007-04-16 ago improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
2007-04-02 ago rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
2007-03-28 ago the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
2007-03-22 ago clarified an error-message
2007-03-12 ago removes some unused code that used to try to derive a simpler version of the eqvt lemmas
2007-03-06 ago major update of the nominal package; there is now an infrastructure
2007-02-08 ago added get-functions
2007-02-06 ago fixed two stupid bugs of SML to do with the value restriction and missing type
2007-02-06 ago moved the infrastructure from the nominal_tags file to nominal_thmdecls