1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Feb 26 06:21:31 2009 -0800
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Feb 26 06:33:48 2009 -0800
     1.3 @@ -5926,7 +5926,7 @@
     1.4  apply mir
     1.5  done
     1.6  
     1.7 -lemma "ALL x y. \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
     1.8 +lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
     1.9  apply mir
    1.10  done
    1.11