src/HOL/Tools/inductive_set_package.ML
Thu, 19 Jul 2007 15:37:37 +0200 berghofe strong_ind_simproc now only rewrites arguments of inductive predicates.
Wed, 11 Jul 2007 11:43:31 +0200 berghofe New wrapper for defining inductive sets with new inductive
less more (0) tip