src/ZF/ZF.ML
changeset 854 2e3ca37dfa14
parent 825 76d9575950f2
child 868 452f1e6ae3bc
equal deleted inserted replaced
853:a4b286dfdd6f 854:2e3ca37dfa14
   409  (fn [major,minor]=>
   409  (fn [major,minor]=>
   410   [ rtac ([major, equals0I] MRS swap) 1,
   410   [ rtac ([major, equals0I] MRS swap) 1,
   411     swap_res_tac [minor] 1,
   411     swap_res_tac [minor] 1,
   412     assume_tac 1 ]);
   412     assume_tac 1 ]);
   413 
   413 
   414 (*Can replace most uses by eq_cs (which is ZF_cs addSIs [equalityI])*)
       
   415 (*A claset that leaves <= formulae unchanged!*)
   414 (*A claset that leaves <= formulae unchanged!*)
   416 val subset0_cs = FOL_cs
   415 val subset0_cs = FOL_cs
   417   addSIs [ballI, InterI, CollectI, PowI, empty_subsetI]
   416   addSIs [ballI, InterI, CollectI, PowI, empty_subsetI]
   418   addIs [bexI, UnionI, ReplaceI, RepFunI]
   417   addIs [bexI, UnionI, ReplaceI, RepFunI]
   419   addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE,
   418   addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE,