equal
deleted
inserted
replaced
530 rewrite Numeral0 into 0 |
530 rewrite Numeral0 into 0 |
531 rewrite Numeral1 into 1 |
531 rewrite Numeral1 into 1 |
532 *) |
532 *) |
533 |
533 |
534 fun is_strange_number ctxt (t as Const (@{const_name neg_numeral}, _) $ _) = |
534 fun is_strange_number ctxt (t as Const (@{const_name neg_numeral}, _) $ _) = |
535 (case try HOLogic.dest_number t of |
535 SMT_Builtin.is_builtin_num ctxt t |
536 SOME (_, i) => SMT_Builtin.is_builtin_num ctxt t andalso i < 2 |
|
537 | NONE => false) |
|
538 | is_strange_number _ _ = false |
536 | is_strange_number _ _ = false |
539 |
537 |
540 val pos_num_ss = |
538 val pos_num_ss = |
541 simpset_of (put_simpset HOL_ss @{context} |
539 simpset_of (put_simpset HOL_ss @{context} |
542 addsimps [@{thm Num.numeral_One}] |
540 addsimps [@{thm Num.numeral_One}] |