src/HOL/Nominal/nominal_atoms.ML
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
2007-04-24 ago add two lemmas dealing with freshness on permutations.
2007-04-23 ago simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
2007-04-20 ago moved axclass module closer to core system
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-07 ago deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
2007-04-07 ago tuned slightly the previous commit
2007-04-07 ago perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
2007-03-31 ago added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas
2007-03-28 ago made the type sets instance of the "cp" type-class
2007-03-27 ago added extended the lemma for equivariance of freshness
2007-03-06 ago major update of the nominal package; there is now an infrastructure
2007-02-07 ago Adapted to changes in Finite_Set theory.
2006-12-06 ago removed legacy ML bindings;
2006-11-15 ago replaced exists_fresh lemma with a version formulated with obtains;
2006-11-10 ago deleted all uses of sign_of as it's now the identity function
2006-08-14 ago Removed non-trivial definitions from calc_atm theorem list.
2006-07-21 ago adaption to argument change in primrec_package
2006-07-11 ago replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
2006-07-08 ago Goal.prove_global;
2006-07-04 ago added simplification rules to the fresh_guess tactic
2006-07-04 ago made calc_atm stronger by including some relative
2006-07-02 ago added more infrastructure for the recursion combinator
2006-05-15 ago added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
2006-05-13 ago unchecked definitions;
2006-05-05 ago added the lemma abs_fun_eq' to the nominal theory,
2006-05-03 ago added lemma fresh_right, which is useful
2006-04-30 ago AxClass.define_class_i;