| changeset 12486 | 0ed8bdd883e0 |
| parent 11868 | 56db9f3a6b3e |
| child 14251 | b91f632a1d37 |
--- a/src/HOL/Integ/NatSimprocs.ML Thu Dec 13 12:33:23 2001 +0100 +++ b/src/HOL/Integ/NatSimprocs.ML Thu Dec 13 15:45:03 2001 +0100 @@ -101,7 +101,7 @@ Goal "Suc(Suc(m)) mod 2 = m mod 2"; by (subgoal_tac "m mod 2 < 2" 1); by (Asm_simp_tac 2); -be (less_2_cases RS disjE) 1; +by (etac (less_2_cases RS disjE) 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def, mod_Suc, nat_1]))); qed "mod2_Suc_Suc"; Addsimps [mod2_Suc_Suc];