src/HOL/Real.thy
changeset 61076 bdc1e2f0a86a
parent 61070 b72a990adfe2
child 61204 3e491e34a62e
     1.1 --- a/src/HOL/Real.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Real.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -491,7 +491,7 @@
     1.4      by transfer (simp add: ac_simps realrel_def)
     1.5    show "(a + b) * c = a * c + b * c"
     1.6      by transfer (simp add: distrib_right realrel_def)
     1.7 -  show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
     1.8 +  show "(0::real) \<noteq> (1::real)"
     1.9      by transfer (simp add: realrel_def)
    1.10    show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
    1.11      apply transfer
    1.12 @@ -1975,7 +1975,7 @@
    1.13  instantiation real :: equal
    1.14  begin
    1.15  
    1.16 -definition "HOL.equal (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
    1.17 +definition "HOL.equal (x::real) y \<longleftrightarrow> x - y = 0"
    1.18  
    1.19  instance proof
    1.20  qed (simp add: equal_real_def)