src/ZF/ZF.ML
changeset 868 452f1e6ae3bc
parent 854 2e3ca37dfa14
child 1016 2317b680fe58
equal deleted inserted replaced
867:e1a654c29b05 868:452f1e6ae3bc
   403   [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
   403   [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
   404 
   404 
   405 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
   405 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
   406  (fn _ => [REPEAT (ares_tac [notI, equals0D] 1)]);
   406  (fn _ => [REPEAT (ares_tac [notI, equals0D] 1)]);
   407 
   407 
   408 qed_goal "not_emptyE" ZF.thy "[| A ~= 0;  !!x. x:A ==> R |] ==> R";
   408 qed_goal "not_emptyE" ZF.thy "[| A ~= 0;  !!x. x:A ==> R |] ==> R"
   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