changeset 10482 | 41de88cb2108 |
parent 10233 | 08083bd2a64d |
child 10832 | e33b47e4246d |
--- a/src/HOL/Set.ML Fri Nov 17 18:47:33 2000 +0100 +++ b/src/HOL/Set.ML Fri Nov 17 18:48:00 2000 +0100 @@ -240,6 +240,11 @@ Addsimps [UNIV_I]; AddIs [UNIV_I]; (*unsafe makes it less likely to cause problems*) +Goal "EX x. x : UNIV"; +by (Simp_tac 1); +qed "UNIV_witness"; +AddXIs [UNIV_witness]; + Goal "A <= UNIV"; by (rtac subsetI 1); by (rtac UNIV_I 1); @@ -702,6 +707,7 @@ by (rtac (major RS imageE) 1); by (etac minor 1); qed "rangeE"; +AddXEs [rangeE]; (*** Set reasoning tools ***)