src/HOL/Nominal/nominal_thmdecls.ML
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 auxiliary dynamic_thm(s) for fact lookup;
2007-09-13 urbanc 2007-09-13 some cleaning up to do with contexts
2007-08-14 wenzelm 2007-08-14 avoid low-level tsig;
2007-08-14 narboux 2007-08-14 fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
2007-07-29 wenzelm 2007-07-29 renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-16 urbanc 2007-04-16 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 narboux 2007-04-02 rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
2007-03-28 urbanc 2007-03-28 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 urbanc 2007-03-22 clarified an error-message
2007-03-12 narboux 2007-03-12 removes some unused code that used to try to derive a simpler version of the eqvt lemmas
2007-03-06 urbanc 2007-03-06 major update of the nominal package; there is now an infrastructure for equivariance lemmas which eases definitions of nominal functions
2007-02-08 urbanc 2007-02-08 added get-functions
2007-02-06 urbanc 2007-02-06 fixed two stupid bugs of SML to do with the value restriction and missing type information in records
2007-02-06 urbanc 2007-02-06 moved the infrastructure from the nominal_tags file to nominal_thmdecls file, and adapted the code to conform with informal Isabelle programming conventions