changeset 64240 | eabf80376aab |
parent 63664 | 9ddc48a8635e |
child 64246 | 15d1ee6e847b |
--- a/src/HOL/Library/Float.thy Sun Oct 16 09:31:03 2016 +0200 +++ b/src/HOL/Library/Float.thy Sun Oct 16 09:31:04 2016 +0200 @@ -590,7 +590,7 @@ qualified lemma compute_float_sgn[code]: "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)" - by transfer (simp add: sgn_times) + by transfer (simp add: sgn_mult) lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .