src/HOL/Nominal/nominal_induct.ML
Tue, 11 Jul 2006 12:16:57 +0200 wenzelm Name.internal;
Sat, 17 Jun 2006 19:37:43 +0200 wenzelm RuleCases.mutual_rule: ctxt;
Tue, 21 Feb 2006 15:06:50 +0100 wenzelm distinct (op =);
Mon, 13 Feb 2006 17:02:54 +0100 berghofe Adapted to Context.generic syntax.
Sat, 07 Jan 2006 12:28:25 +0100 wenzelm RuleCases.make_nested;
Thu, 05 Jan 2006 17:16:40 +0100 wenzelm proper handling of simultaneous goals and mutual rules;
Thu, 01 Dec 2005 04:46:17 +0100 urbanc changed "fresh:" to "avoiding:" and cleaned up the weakening example
Wed, 30 Nov 2005 15:24:32 +0100 wenzelm added rename_params_rule: recover orginal fresh names in subgoals/cases;
Wed, 30 Nov 2005 14:27:50 +0100 wenzelm fresh: frees instead of terms, rename corresponding params in rule;
Wed, 30 Nov 2005 00:46:08 +0100 wenzelm proper treatment of tuple/tuple_fun -- nest to the left!
Tue, 29 Nov 2005 18:09:12 +0100 wenzelm reworked version with proper support for defs, fixes, fresh specification;
Sun, 27 Nov 2005 05:09:43 +0100 urbanc some minor tunings
Sun, 13 Nov 2005 22:36:30 +0100 urbanc changed the HOL_basic_ss back and selectively added
Sun, 13 Nov 2005 20:33:36 +0100 urbanc exchanged HOL_ss for HOL_basic_ss in the simplification
Mon, 07 Nov 2005 10:47:25 +0100 urbanc fixed bug with nominal induct
Tue, 01 Nov 2005 23:54:29 +0100 urbanc tunings of some comments (nothing serious)
Mon, 17 Oct 2005 12:30:57 +0200 berghofe Initial revision.
less more (0) tip