# HG changeset patch
# User obua
# Date 1190282949 -7200
# Node ID 3d3ebc0c927c3f5b369e66f831e60ce880eb3f91
# Parent  22b657bee22d5301cd9cd78fec08f5f50d911495
changed lemmas

diff -r 22b657bee22d -r 3d3ebc0c927c src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Wed Sep 19 20:45:29 2007 +0200
+++ b/src/HOL/Real/Float.thy	Thu Sep 20 12:09:09 2007 +0200
@@ -570,7 +570,7 @@
   zpower_Pls zpower_Min
 
 lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 
-          float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound float_add_assoc1 float_add_assoc2
+          float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound
 
 (* for use with the compute oracle *)
 lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false