| changeset 5137 | 60205b0de9b9 |
| parent 5116 | 8eb343ab5748 |
| child 5147 | 825877190618 |
--- a/src/ZF/OrderArith.ML Mon Jul 13 16:42:27 1998 +0200 +++ b/src/ZF/OrderArith.ML Mon Jul 13 16:43:57 1998 +0200 @@ -142,7 +142,7 @@ by (blast_tac (claset() addSIs [if_type]) 2); by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1)); by Safe_tac; -by (ALLGOALS (asm_simp_tac (simpset() addsplits [split_if]))); +by (ALLGOALS Asm_simp_tac); by (blast_tac (claset() addEs [equalityE]) 1); qed "sum_disjoint_bij";