equal
deleted
inserted
replaced
445 (fn prems=> [ blast_tac (claset() addDs prems) 1 ]); |
445 (fn prems=> [ blast_tac (claset() addDs prems) 1 ]); |
446 |
446 |
447 qed_goal "equals0E" ZF.thy "!!P. [| A=0; a:A |] ==> P" |
447 qed_goal "equals0E" ZF.thy "!!P. [| A=0; a:A |] ==> P" |
448 (fn _=> [ Full_simp_tac 1, Blast_tac 1 ]); |
448 (fn _=> [ Full_simp_tac 1, Blast_tac 1 ]); |
449 |
449 |
|
450 AddEs [equals0E, sym RS equals0E]; |
|
451 |
450 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0" |
452 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0" |
451 (fn _=> [ Blast_tac 1 ]); |
453 (fn _=> [ Blast_tac 1 ]); |
452 |
454 |
453 qed_goal "not_emptyE" ZF.thy "[| A ~= 0; !!x. x:A ==> R |] ==> R" |
455 qed_goal "not_emptyE" ZF.thy "[| A ~= 0; !!x. x:A ==> R |] ==> R" |
454 (fn [major,minor]=> |
456 (fn [major,minor]=> |