src/HOL/WF.ML
changeset 5521 7970832271cc
parent 5452 b38332431a8c
child 5579 32f99ca617b7
     1.1 --- a/src/HOL/WF.ML	Mon Sep 21 23:06:37 1998 +0200
     1.2 +++ b/src/HOL/WF.ML	Mon Sep 21 23:12:31 1998 +0200
     1.3 @@ -177,7 +177,7 @@
     1.4    by (Blast_tac 1);
     1.5   by (blast_tac (claset() addEs [equalityE]) 1);
     1.6  by (Asm_full_simp_tac 1);
     1.7 -by (Fast_tac 1);  (*faster than Blast_tac*)
     1.8 +by (fast_tac (claset() delWrapper "bspec") 1); (*faster than Blast_tac*)
     1.9  qed "wf_UN";
    1.10  
    1.11  Goalw [Union_def]