src/HOL/WF.ML
changeset 5337 2f7d09a927c4
parent 5330 8c9fadda81f4
child 5452 b38332431a8c
     1.1 --- a/src/HOL/WF.ML	Wed Aug 19 10:27:25 1998 +0200
     1.2 +++ b/src/HOL/WF.ML	Wed Aug 19 10:27:49 1998 +0200
     1.3 @@ -176,11 +176,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 (case_tac "? i. i:I" 1);
     1.8 - by (Clarify_tac 1);
     1.9 - by (EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
    1.10 - by (Blast_tac 1);
    1.11 -by (Blast_tac 1);
    1.12 +by (Fast_tac 1);  (*faster than Blast_tac*)
    1.13  qed "wf_UN";
    1.14  
    1.15  Goalw [Union_def]