src/HOL/Set.ML
changeset 2935 998cb95fdd43
parent 2912 3fac3e8d5d3e
child 3222 726a9b069947
     1.1 --- a/src/HOL/Set.ML	Fri Apr 11 11:33:51 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Apr 11 15:21:36 1997 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4  
     1.5  qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
     1.6   (fn [prem]=>
     1.7 -  [ (fast_tac (!claset addIs [prem RS FalseE]) 1) ]);
     1.8 +  [ (blast_tac (!claset addIs [prem RS FalseE]) 1) ]);
     1.9  
    1.10  qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
    1.11   (fn _ => [ (Blast_tac 1) ]);
    1.12 @@ -418,7 +418,7 @@
    1.13  (fn _ => [Blast_tac 1]);
    1.14  
    1.15  goal Set.thy "!!a b. {a}={b} ==> a=b";
    1.16 -by (fast_tac (!claset addEs [equalityE]) 1);
    1.17 +by (blast_tac (!claset addEs [equalityE]) 1);
    1.18  qed "singleton_inject";
    1.19  
    1.20  (*Redundant? But unlike insertCI, it proves the subgoal immediately!*)
    1.21 @@ -622,11 +622,11 @@
    1.22  AddSEs [imageE]; 
    1.23  
    1.24  goalw thy [o_def] "(f o g)``r = f``(g``r)";
    1.25 -by (Fast_tac 1);
    1.26 +by (Blast_tac 1);
    1.27  qed "image_compose";
    1.28  
    1.29  goal thy "f``(A Un B) = f``A Un f``B";
    1.30 -by (Fast_tac 1);
    1.31 +by (Blast_tac 1);
    1.32  qed "image_Un";
    1.33  
    1.34