src/HOL/Real.thy
changeset 62348 9a5f43dac883
parent 62347 2230b7047376
child 62390 842917225d56
child 62397 5ae24f33d343
     1.1 --- a/src/HOL/Real.thy	Wed Feb 17 21:51:57 2016 +0100
     1.2 +++ b/src/HOL/Real.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -1282,7 +1282,7 @@
     1.4        @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1},
     1.5        @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff},
     1.6        @{thm of_int_mult}, @{thm of_int_of_nat_eq},
     1.7 -      @{thm of_nat_numeral}, @{thm int_numeral}, @{thm of_int_neg_numeral}]
     1.8 +      @{thm of_nat_numeral}, @{thm of_nat_numeral}, @{thm of_int_neg_numeral}]
     1.9    #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat \<Rightarrow> real"})
    1.10    #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \<Rightarrow> real"}))
    1.11  \<close>