src/ZF/AC/AC16_WO4.ML
changeset 5470 855654b691db
parent 5314 c061e6f9d546
child 6021 4a3fc834288e
--- a/src/ZF/AC/AC16_WO4.ML	Thu Sep 10 17:42:02 1998 +0200
+++ b/src/ZF/AC/AC16_WO4.ML	Thu Sep 10 17:42:44 1998 +0200
@@ -256,7 +256,7 @@
 AddSIs [Infinite];   (*if notI is removed!*)
 AddSEs [Infinite RS notE];
 
-AddEs [IntI RS (disjoint RS equals0E)];
+AddEs [[disjoint, IntI] MRS (equals0D RS notE)];
 
 (*use k = succ(l) *)
 val includes_l = simplify (FOL_ss addsimps [k_def]) includes;