# HG changeset patch
# User immler
# Date 1387210102 -3600
# Node ID 25860d89a044fbcc0373f2af9210e8a366962d58
# Parent  cd8f55c358c5245fbf6c26bfa84d90f88f080bf4
Float: prevent unnecessary large numbers when adding 0

diff -r cd8f55c358c5 -r 25860d89a044 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Library/Float.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -452,7 +452,8 @@
 hide_fact (open) compute_float_times
 
 lemma compute_float_plus[code]: "Float m1 e1 + Float m2 e2 =
-  (if e1 \<le> e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1
+  (if m1 = 0 then Float m2 e2 else if m2 = 0 then Float m1 e1 else
+  if e1 \<le> e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1
               else Float (m2 + m1 * 2^nat (e1 - e2)) e2)"
   by transfer (simp add: field_simps powr_realpow[symmetric] powr_divide2[symmetric])
 hide_fact (open) compute_float_plus