changeset 965 | 24eef3860714 |
parent 923 | ff1574a81019 |
child 972 | e61b058d58d2 |
--- a/src/HOL/Arith.ML Fri Mar 17 22:46:26 1995 +0100 +++ b/src/HOL/Arith.ML Mon Mar 20 15:35:28 1995 +0100 @@ -241,7 +241,7 @@ by (ALLGOALS(asm_simp_tac arith_ss)); qed "Suc_diff_n"; -goal Arith.thy "Suc(m)-n = if (m<n) 0 (Suc m-n)"; +goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc m-n)"; by(simp_tac (nat_ss addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n] setloop (split_tac [expand_if])) 1); qed "if_Suc_diff_n";