Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Matrix_LP/ComputeFloat.thy
changeset 63901 4ce989e962e0
parent 63167 0909deb8059b
child 65583 8d53b3bebab4 
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -46,7 +46,7 @@
 apply (simp add: int_of_real_sub real_int_of_real)
 done
 
-lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real_of_int a = x"
+lemma real_is_int_rep: "real_is_int x \<Longrightarrow> \<exists>!(a::int). real_of_int a = x"
 by (auto simp add: real_is_int_def)
 
 lemma int_of_real_mult:
isabelle