equal
deleted
inserted
replaced
26 where "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))" |
26 where "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))" |
27 |
27 |
28 lemmas compute_natarith = |
28 lemmas compute_natarith = |
29 arith_simps rel_simps |
29 arith_simps rel_simps |
30 diff_nat_numeral nat_numeral nat_0 nat_neg_numeral |
30 diff_nat_numeral nat_numeral nat_0 nat_neg_numeral |
31 numeral_1_eq_1 [symmetric] |
31 numeral_One [symmetric] |
32 numeral_1_eq_Suc_0 [symmetric] |
32 numeral_1_eq_Suc_0 [symmetric] |
33 Suc_numeral natfac.simps |
33 Suc_numeral natfac.simps |
34 |
34 |
35 lemmas number_norm = numeral_1_eq_1[symmetric] |
35 lemmas number_norm = numeral_One[symmetric] |
36 |
36 |
37 lemmas compute_numberarith = |
37 lemmas compute_numberarith = |
38 arith_simps rel_simps number_norm |
38 arith_simps rel_simps number_norm |
39 |
39 |
40 lemmas compute_num_conversions = |
40 lemmas compute_num_conversions = |