src/HOL/Rat.thy
changeset 61144 5e94dfead1c2
parent 61070 b72a990adfe2
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Rat.thy	Wed Sep 09 14:47:41 2015 +0200
     1.2 +++ b/src/HOL/Rat.thy	Wed Sep 09 20:57:21 2015 +0200
     1.3 @@ -629,7 +629,7 @@
     1.4        @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
     1.5        @{thm of_int_minus}, @{thm of_int_diff},
     1.6        @{thm of_int_of_nat_eq}]
     1.7 -  #> Lin_Arith.add_simprocs Numeral_Simprocs.field_divide_cancel_numeral_factor
     1.8 +  #> Lin_Arith.add_simprocs [Numeral_Simprocs.field_divide_cancel_numeral_factor]
     1.9    #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
    1.10    #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
    1.11  \<close>