Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add type annotation
authorhuffman
Thu, 26 Feb 2009 06:33:48 -0800
changeset 30103 32effb2a8168
parent 30102 799b687e4aac
child 30104 b094999e1d33
add type annotation
src/HOL/Decision_Procs/MIR.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Decision_Procs/MIR.thy	Thu Feb 26 06:21:31 2009 -0800
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu Feb 26 06:33:48 2009 -0800
@@ -5926,7 +5926,7 @@
 apply mir
 done
 
-lemma "ALL x y. \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
+lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
 apply mir
 done
isabelle