src/HOL/Matrix_LP/ComputeFloat.thy
changeset 63901 4ce989e962e0
parent 63167 0909deb8059b
child 65583 8d53b3bebab4
     1.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  apply (simp add: int_of_real_sub real_int_of_real)
     1.5  done
     1.6  
     1.7 -lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real_of_int a = x"
     1.8 +lemma real_is_int_rep: "real_is_int x \<Longrightarrow> \<exists>!(a::int). real_of_int a = x"
     1.9  by (auto simp add: real_is_int_def)
    1.10  
    1.11  lemma int_of_real_mult: