| 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]