src/ZF/ZF.ML
changeset 854 2e3ca37dfa14
parent 825 76d9575950f2
child 868 452f1e6ae3bc
--- a/src/ZF/ZF.ML	Thu Jan 12 03:02:05 1995 +0100
+++ b/src/ZF/ZF.ML	Thu Jan 12 03:02:34 1995 +0100
@@ -411,7 +411,6 @@
     swap_res_tac [minor] 1,
     assume_tac 1 ]);
 
-(*Can replace most uses by eq_cs (which is ZF_cs addSIs [equalityI])*)
 (*A claset that leaves <= formulae unchanged!*)
 val subset0_cs = FOL_cs
   addSIs [ballI, InterI, CollectI, PowI, empty_subsetI]