equal
deleted
inserted
replaced
846 end; |
846 end; |
847 |
847 |
848 val nat_exp_ss = |
848 val nat_exp_ss = |
849 simpset_of |
849 simpset_of |
850 (put_simpset HOL_basic_ss @{context} |
850 (put_simpset HOL_basic_ss @{context} |
851 addsimps (@{thms eval_nat_numeral} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps}) |
851 addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps}) |
852 addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]); |
852 addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]); |
853 |
853 |
854 fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; |
854 fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; |
855 |
855 |
856 |
856 |