equal
deleted
inserted
replaced
598 lessD = lessD @ [zless_imp_add1_zle], |
598 lessD = lessD @ [zless_imp_add1_zle], |
599 neqE = neqE, |
599 neqE = neqE, |
600 simpset = simpset addsimps add_rules |
600 simpset = simpset addsimps add_rules |
601 addsimprocs Int_Numeral_Base_Simprocs |
601 addsimprocs Int_Numeral_Base_Simprocs |
602 addcongs [if_weak_cong]}) #> |
602 addcongs [if_weak_cong]}) #> |
603 arith_inj_const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) #> |
603 arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #> |
604 arith_discrete "IntDef.int" |
604 arith_discrete "IntDef.int" |
605 |
605 |
606 end; |
606 end; |
607 |
607 |
608 val fast_int_arith_simproc = |
608 val fast_int_arith_simproc = |