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