src/HOL/subset.ML
changeset 1760 6f41a494f3b1
parent 1631 26570790f089
child 1761 29e08d527ba1
     1.1 --- a/src/HOL/subset.ML	Wed May 22 18:32:37 1996 +0200
     1.2 +++ b/src/HOL/subset.ML	Thu May 23 14:37:06 1996 +0200
     1.3 @@ -13,11 +13,11 @@
     1.4   (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
     1.5  
     1.6  goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
     1.7 -by (fast_tac set_cs 1);
     1.8 +by (Fast_tac 1);
     1.9  qed "subset_insert";
    1.10  
    1.11  qed_goal "subset_empty_iff" Set.thy "(A<={}) = (A={})"
    1.12 - (fn _=> [ (fast_tac (set_cs addIs [equalityI]) 1) ]);
    1.13 + (fn _=> [ (fast_tac (!claset addIs [equalityI]) 1) ]);
    1.14  
    1.15  (*** Big Union -- least upper bound of a set  ***)
    1.16