src/HOL/Nominal/nominal_package.ML
changeset 21669 c68717c16013
parent 21540 f3faed8276e6
child 21858 05f57309170c
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Dec 05 22:14:53 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Dec 06 01:12:36 2006 +0100
     1.3 @@ -18,6 +18,18 @@
     1.4  structure NominalPackage : NOMINAL_PACKAGE =
     1.5  struct
     1.6  
     1.7 +val Finites_emptyI = thm "Finites.emptyI";
     1.8 +val finite_Diff = thm "finite_Diff";
     1.9 +val finite_Un = thm "finite_Un";
    1.10 +val Un_iff = thm "Un_iff";
    1.11 +val In0_eq = thm "In0_eq";
    1.12 +val In1_eq = thm "In1_eq";
    1.13 +val In0_not_In1 = thm "In0_not_In1";
    1.14 +val In1_not_In0 = thm "In1_not_In0";
    1.15 +val Un_assoc = thm "Un_assoc";
    1.16 +val Collect_disj_eq = thm "Collect_disj_eq";
    1.17 +val empty_def = thm "empty_def";
    1.18 +
    1.19  open DatatypeAux;
    1.20  open NominalAtoms;
    1.21  
    1.22 @@ -1004,7 +1016,7 @@
    1.23              (fn _ =>
    1.24                simp_tac (HOL_basic_ss addsimps (supp_def ::
    1.25                   Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
    1.26 -                 symmetric empty_def :: Finites.emptyI :: simp_thms @
    1.27 +                 symmetric empty_def :: Finites_emptyI :: simp_thms @
    1.28                   abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
    1.29          in
    1.30            (supp_thm,