equal
deleted
inserted
replaced
51 @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, |
51 @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, |
52 @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less}, |
52 @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less}, |
53 @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, |
53 @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, |
54 @{thm less_nat_number_of}, |
54 @{thm less_nat_number_of}, |
55 @{thm Let_number_of}, @{thm nat_number_of}] @ |
55 @{thm Let_number_of}, @{thm nat_number_of}] @ |
56 @{thms arith_simps} @ @{thms rel_simps}; |
56 @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps}; |
57 |
57 |
58 fun prep_simproc (name, pats, proc) = |
58 fun prep_simproc (name, pats, proc) = |
59 Simplifier.simproc (the_context ()) name pats proc; |
59 Simplifier.simproc (the_context ()) name pats proc; |
60 |
60 |
61 |
61 |