Renamed equals0D to equals0E
authorpaulson
Wed Aug 05 11:00:48 1998 +0200 (1998-08-05)
changeset 5256e6983301ce5e
parent 5255 e29e77ad7b91
child 5257 c03e3ba9cbcc
Renamed equals0D to equals0E
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Wed Aug 05 11:00:21 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Wed Aug 05 11:00:48 1998 +0200
     1.3 @@ -252,13 +252,19 @@
     1.4  qed_goal "empty_subsetI" Set.thy "{} <= A"
     1.5   (fn _ => [ (Blast_tac 1) ]);
     1.6  
     1.7 +(*One effect is to delete the ASSUMPTION {} <= A*)
     1.8 +AddIffs [empty_subsetI];
     1.9 +
    1.10  qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
    1.11   (fn [prem]=>
    1.12    [ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]);
    1.13  
    1.14 -qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
    1.15 +(*Use for reasoning about disjointness: A Int B = {} *)
    1.16 +qed_goal "equals0E" Set.thy "!!a. [| A={};  a:A |] ==> P"
    1.17   (fn _ => [ (Blast_tac 1) ]);
    1.18  
    1.19 +AddEs [equals0E];
    1.20 +
    1.21  Goalw [Ball_def] "Ball {} P = True";
    1.22  by (Simp_tac 1);
    1.23  qed "ball_empty";
    1.24 @@ -669,7 +675,7 @@
    1.25  simpset_ref() := simpset() addcongs [ball_cong,bex_cong]
    1.26                      setmksimps (mksimps mksimps_pairs);
    1.27  
    1.28 -Addsimps[subset_UNIV, empty_subsetI, subset_refl];
    1.29 +Addsimps[subset_UNIV, subset_refl];
    1.30  
    1.31  
    1.32  (*** < ***)