src/HOL/Nominal/nominal_induct.ML
2009-03-16 ago simplified method setup;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-02-25 ago Added lemmas for normalizing freshness results involving fresh_star.
2009-01-21 ago binding is alias for Binding.T
2008-12-04 ago cleaned up binding module and related code
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-09 ago unified Args.T with OuterLex.token, renamed some operations;
2008-06-26 ago Args.context;
2008-05-18 ago guess_instance: proper context;
2008-04-17 ago adapted to ProofContext.revert_skolem: extra Name.clean required;
2008-01-26 ago avoid redundant escaping of Isabelle symbols;
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-10-04 ago moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-07-05 ago simplified ObjectLogic.atomize;
2007-01-16 ago added capabilities to handle mutual inductions
2006-12-18 ago switched argument order in *.syntax lifters
2006-10-12 ago To be consistent with "induct", I renamed "fixing" to "arbitrary".
2006-08-02 ago simplified Assumption/ProofContext.export;
2006-07-11 ago Name.internal;
2006-06-17 ago RuleCases.mutual_rule: ctxt;
2006-02-21 ago distinct (op =);
2006-02-13 ago Adapted to Context.generic syntax.
2006-01-07 ago RuleCases.make_nested;
2006-01-05 ago proper handling of simultaneous goals and mutual rules;
2005-12-01 ago changed "fresh:" to "avoiding:" and cleaned up the weakening example
2005-11-30 ago added rename_params_rule: recover orginal fresh names in subgoals/cases;
2005-11-30 ago fresh: frees instead of terms, rename corresponding params in rule;
2005-11-30 ago proper treatment of tuple/tuple_fun -- nest to the left!
2005-11-29 ago reworked version with proper support for defs, fixes, fresh specification;
2005-11-27 ago some minor tunings
2005-11-13 ago changed the HOL_basic_ss back and selectively added
2005-11-13 ago exchanged HOL_ss for HOL_basic_ss in the simplification
2005-11-07 ago fixed bug with nominal induct
2005-11-01 ago tunings of some comments (nothing serious)
2005-10-17 ago Initial revision.