src/HOL/Nominal/nominal_induct.ML
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
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-05-30 wenzelm 2015-05-30 tuned -- more direct Thm.renamed_prop;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-03-06 wenzelm 2015-03-06 clarified 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;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-08-19 wenzelm 2014-08-19 simplified type Proof.method;
2014-03-06 wenzelm 2014-03-06 tuned;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-08-23 wenzelm 2013-08-23 tuned signature;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-11-03 wenzelm 2011-11-03 tuned signature;
2011-10-12 wenzelm 2011-10-12 tuned signature;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-01-10 berghofe 2010-01-10 Added infrastructure for simplifying equality constraints. Option (no_simp) restores old behaviour of induct method.
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-02-25 berghofe 2009-02-25 Added lemmas for normalizing freshness results involving fresh_star.
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-06-26 wenzelm 2008-06-26 Args.context;
2008-05-18 wenzelm 2008-05-18 guess_instance: proper context;
2008-04-17 wenzelm 2008-04-17 adapted to ProofContext.revert_skolem: extra Name.clean required;
2008-01-26 wenzelm 2008-01-26 avoid redundant escaping of Isabelle symbols;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-07-05 wenzelm 2007-07-05 simplified ObjectLogic.atomize;
2007-01-16 urbanc 2007-01-16 added capabilities to handle mutual inductions
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-10-12 urbanc 2006-10-12 To be consistent with "induct", I renamed "fixing" to "arbitrary". However I am not very fond of "arbitrary" - e.g. it clashes with "arbitrary" of HOL. Both Gentzen (at least in the Szabo translation) and Velleman (in How to prove it: a structured approach) use "arbitrary". Still, I wonder whether "generalising" is a good compromise?
2006-08-02 wenzelm 2006-08-02 simplified Assumption/ProofContext.export;
2006-07-11 wenzelm 2006-07-11 Name.internal;
2006-06-17 wenzelm 2006-06-17 RuleCases.mutual_rule: ctxt; Term.internal; ProofContext.exports: simultaneous facts;
2006-02-21 wenzelm 2006-02-21 distinct (op =); removed spurious PolyML.print;
2006-02-13 berghofe 2006-02-13 Adapted to Context.generic syntax.
2006-01-07 wenzelm 2006-01-07 RuleCases.make_nested;
2006-01-05 wenzelm 2006-01-05 proper handling of simultaneous goals and mutual rules;
2005-12-01 urbanc 2005-12-01 changed "fresh:" to "avoiding:" and cleaned up the weakening example
2005-11-30 wenzelm 2005-11-30 added rename_params_rule: recover orginal fresh names in subgoals/cases;
2005-11-30 wenzelm 2005-11-30 fresh: frees instead of terms, rename corresponding params in rule; tuned;
2005-11-30 wenzelm 2005-11-30 proper treatment of tuple/tuple_fun -- nest to the left!
2005-11-29 wenzelm 2005-11-29 reworked version with proper support for defs, fixes, fresh specification;
2005-11-27 urbanc 2005-11-27 some minor tunings
2005-11-13 urbanc 2005-11-13 changed the HOL_basic_ss back and selectively added simp_thms and triv_forall_equality. (Otherwise the goals would have been simplified too much)
2005-11-13 urbanc 2005-11-13 exchanged HOL_ss for HOL_basic_ss in the simplification part. Otherwise the case where the context is instantiated with unit leads to vacuous quantifiers, such as ALL a. A