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
2005-11-07 urbanc 2005-11-07 fixed bug with nominal induct - the bug occured in rule inductions when the goal did not use all variables from the relation over which the induction was done
2005-11-01 urbanc 2005-11-01 tunings of some comments (nothing serious)
2005-10-17 berghofe 2005-10-17 Initial revision.