src/HOL/Nominal/nominal_induct.ML
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.