src/HOL/Nominal/nominal_thmdecls.ML
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-07-26 wenzelm 2015-07-26 updated to infer_instantiate; clarified context;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-04-09 wenzelm 2014-04-09 proper context for print_tac;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-01-11 wenzelm 2014-01-11 tuned signature;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 wenzelm 2010-08-27 more antiquotations;
2010-08-27 wenzelm 2010-08-27 eliminated Unsynchronized.ref in favour of configuration option; proper naming of thy: theory vs. ctxt: Proof.context; recovered some Isabelle/ML indendation style;
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
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