src/HOL/Nominal/nominal_atoms.ML
2011-10-12 ago modernized structure Induct_Tacs;
2011-09-03 ago tuned specifications
2011-09-03 ago assert Pure equations for theorem references; tuned
2011-01-15 ago Finally removed old primrec package, since Primrec.add_primrec_global
2010-12-15 ago eliminated dead code;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-07-01 ago "prod" and "sum" replace "*" and "+" respectively
2010-06-10 ago tuned quotes, antiquotations and whitespace
2010-05-17 ago prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
2009-11-08 ago adapted Theory_Data;
2009-10-17 ago eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-15 ago replaced String.concat by implode;
2009-06-23 ago tuned interfaces of datatype module
2009-06-23 ago add_datatypes does not yield particular rules any longer
2009-06-23 ago add_datatype interface yields type names and less rules
2009-06-21 ago simplified names of common datatype types
2009-06-19 ago discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-17 ago datatype packages: record datatype_config for configuration flags; less verbose signatures
2009-05-07 ago explicit type_name antiquotations
2009-03-19 ago proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
2009-03-07 ago more uniform handling of binding in packages;
2009-03-04 ago Made Option a separate theory and renamed option_map to Option.map
2009-02-25 ago Added equivariance lemmas for fresh_star.
2009-01-21 ago binding replaces bstring
2008-12-16 ago changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
2008-12-04 ago cleaned up binding module and related code
2008-11-10 ago Some more functions for accessing information about atoms.
2008-09-26 ago Added some more theorems to NominalData.
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-27 ago added equivariance lemmas for ex1 and the
2008-07-29 ago PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-06-30 ago added facts to lemma swap_simps and tuned lemma calc_atms
2008-06-14 ago InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;
2008-06-10 ago InductTacs.case_tac with proper context and proper declaration of local variable;
2008-06-10 ago polished interface of datatype package
2008-06-09 ago adapted case_tac/induct_tac;
2008-05-07 ago - Deleted arity proofs for set
2008-05-02 ago added more infrastructure for fresh_star
2008-03-29 ago eliminated non-linear access to thy1 and thy12c;
2008-03-25 ago removed redundant axiomatizations of XXX_infinite (fact already proven);
2008-03-20 ago simplified get_thm(s): back to plain name argument;
2008-03-19 ago auxiliary dynamic_thm(s) for fact lookup;
2008-02-18 ago added eqvt-flag to subseteq-lemma
2008-01-15 ago joined theories IntDef, Numeral, IntArith to theory Int
2007-12-06 ago added new primrec package
2007-12-05 ago map_product and fold_product
2007-10-06 ago simplified interfaces for outer syntax;
2007-09-25 ago proper Sign operations instead of Theory aliases;
2007-09-23 ago changed the representation of atoms to datatypes over nats
2007-09-13 ago Added equivariance lemmas for induct_forall.
2007-09-05 ago modified proofs so that they are not using claset()
2007-08-10 ago ClassPackage renamed to Class
2007-08-09 ago re-eliminated Option.thy
2007-08-07 ago split off theory Option for benefit of code generator
2007-07-21 ago tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-05-31 ago introduced symmetric variants of the lemmas for alpha-equivalence
2007-05-19 ago constant op @ now named append
2007-05-07 ago simplified DataFun interfaces;
2007-04-25 ago add the lemma supp_eqvt and put the right attribute
2007-04-24 ago fixes last commit