| changeset 5521 | 7970832271cc |
| parent 5490 | 85855f65d0c6 |
| child 5590 | 477fc12adceb |
--- a/src/HOL/equalities.ML Mon Sep 21 23:06:37 1998 +0200 +++ b/src/HOL/equalities.ML Mon Sep 21 23:12:31 1998 +0200 @@ -722,8 +722,7 @@ qed "ex_bool_eq"; Goal "A Un B = (UN b. if b then A else B)"; -by Auto_tac; -by (asm_full_simp_tac (simpset() addsimps [split_if_mem2]) 1); +by(auto_tac(claset()delWrapper"bspec",simpset()addsimps [split_if_mem2])); qed "Un_eq_UN"; Goal "(UN b::bool. A b) = (A True Un A False)";