src/HOL/Nominal/nominal_package.ML
changeset 17873 09236f6a6a19
parent 17872 f08fc98a164a
child 17874 8be65cf94d2e
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 17:42:24 2005 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 18:34:51 2005 +0200
     1.3 @@ -1769,6 +1769,7 @@
     1.4              (fn _ =>
     1.5                [simp_tac (HOL_basic_ss addsimps (supp_def ::
     1.6                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
     1.7 +                 refl :: symmetric empty_def :: Finites.emptyI :: simp_thms @
     1.8                   abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1])
     1.9          in
    1.10            (supp_thm,