src/HOL/Decision_Procs/MIR.thy
changeset 41882 ae8d62656392
parent 41849 1a65b780bd56
child 41891 d37babdf5cae
equal deleted inserted replaced
41881:ea4d8dc12ed5 41882:ae8d62656392
  5619 
  5619 
  5620 lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
  5620 lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1"
  5621 apply mir
  5621 apply mir
  5622 done
  5622 done
  5623 
  5623 
  5624 unused_thms
       
  5625 
       
  5626 end
  5624 end