src/HOL/subset.ML
changeset 1631 26570790f089
parent 1552 6f71b5d46700
child 1760 6f41a494f3b1
     1.1 --- a/src/HOL/subset.ML	Fri Mar 29 11:38:47 1996 +0100
     1.2 +++ b/src/HOL/subset.ML	Fri Mar 29 13:16:38 1996 +0100
     1.3 @@ -16,6 +16,9 @@
     1.4  by (fast_tac set_cs 1);
     1.5  qed "subset_insert";
     1.6  
     1.7 +qed_goal "subset_empty_iff" Set.thy "(A<={}) = (A={})"
     1.8 + (fn _=> [ (fast_tac (set_cs addIs [equalityI]) 1) ]);
     1.9 +
    1.10  (*** Big Union -- least upper bound of a set  ***)
    1.11  
    1.12  val prems = goal Set.thy