src/HOL/subset.ML
changeset 1761 29e08d527ba1
parent 1760 6f41a494f3b1
child 2515 6ff9bd353121
     1.1 --- a/src/HOL/subset.ML	Thu May 23 14:37:06 1996 +0200
     1.2 +++ b/src/HOL/subset.ML	Thu May 23 15:15:20 1996 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  qed "subset_insert";
     1.5  
     1.6  qed_goal "subset_empty_iff" Set.thy "(A<={}) = (A={})"
     1.7 - (fn _=> [ (fast_tac (!claset addIs [equalityI]) 1) ]);
     1.8 + (fn _=> [ (Fast_tac 1) ]);
     1.9  
    1.10  (*** Big Union -- least upper bound of a set  ***)
    1.11