src/HOL/Nominal/nominal_thmdecls.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated old Display.print_cterm;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-04-27 Christian Urban 2009-04-27 tuned
2009-04-26 Christian Urban 2009-04-26 deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-02-25 berghofe 2009-02-25 Replaced Logic.unvarify by Variable.import_terms to make declaration of equivariance lemmas work in locales.
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-15 wenzelm 2008-04-15 proper dynamic facts for eqvts, freshs, bijs; removed obsolete print_data -- facts are accesivle via regular names; misc tuning/simplification;
2008-03-25 wenzelm 2008-03-25 update_context: always store as "Nominal.eqvts"; added dynamic fact bindings for "eqvts", "freshs", "bijs";
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