equal
deleted
inserted
replaced
522 simpset = simpset addsimps add_rules |
522 simpset = simpset addsimps add_rules |
523 addsimprocs simprocs |
523 addsimprocs simprocs |
524 addcongs [if_weak_cong]}), |
524 addcongs [if_weak_cong]}), |
525 arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT), |
525 arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT), |
526 arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT), |
526 arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT), |
527 arith_discrete ("IntDef.int", true)]; |
527 arith_discrete "IntDef.int"]; |
528 |
528 |
529 end; |
529 end; |
530 |
530 |
531 val fast_int_arith_simproc = |
531 val fast_int_arith_simproc = |
532 Simplifier.simproc (Theory.sign_of (the_context())) |
532 Simplifier.simproc (Theory.sign_of (the_context())) |