| changeset 30103 | 32effb2a8168 |
| parent 30097 | 57df8626c23b |
| child 30242 | aea5d7fa7ef5 |
--- 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