equal
deleted
inserted
replaced
59 zerone_conv |
59 zerone_conv |
60 (Simplifier.rewrite |
60 (Simplifier.rewrite |
61 (HOL_basic_ss |
61 (HOL_basic_ss |
62 addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps} |
62 addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps} |
63 @ [if_False, if_True, @{thm add_0}, @{thm add_Suc}, |
63 @ [if_False, if_True, @{thm add_0}, @{thm add_Suc}, |
64 @{thm add_number_of_left}, @{thm Suc_eq_add_numeral_1}] |
64 @{thm add_number_of_left}, @{thm Suc_eq_plus1}] |
65 @ map (fn th => th RS sym) @{thms numerals})); |
65 @ map (fn th => th RS sym) @{thms numerals})); |
66 |
66 |
67 val nat_mul_conv = nat_add_conv; |
67 val nat_mul_conv = nat_add_conv; |
68 val zeron_tm = @{cterm "0::nat"}; |
68 val zeron_tm = @{cterm "0::nat"}; |
69 val onen_tm = @{cterm "1::nat"}; |
69 val onen_tm = @{cterm "1::nat"}; |