src/HOL/Library/Float.thy
changeset 55565 f663fc1e653b
parent 54784 54f1ce13c140
child 55945 e96383acecf9
     1.1 --- a/src/HOL/Library/Float.thy	Tue Feb 18 23:03:49 2014 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Tue Feb 18 23:03:50 2014 +0100
     1.3 @@ -161,11 +161,11 @@
     1.4  lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
     1.5  declare sgn_float.rep_eq[simp]
     1.6  
     1.7 -lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" ..
     1.8 +lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" .
     1.9  
    1.10 -lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" ..
    1.11 +lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" .
    1.12  declare less_eq_float.rep_eq[simp]
    1.13 -lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" ..
    1.14 +lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" .
    1.15  declare less_float.rep_eq[simp]
    1.16  
    1.17  instance
    1.18 @@ -466,7 +466,7 @@
    1.19    by transfer (simp add: sgn_times)
    1.20  hide_fact (open) compute_float_sgn
    1.21  
    1.22 -lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" ..
    1.23 +lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .
    1.24  
    1.25  lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
    1.26    by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])
    1.27 @@ -476,7 +476,7 @@
    1.28    by transfer (simp add: field_simps)
    1.29  hide_fact (open) compute_float_less
    1.30  
    1.31 -lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" ..
    1.32 +lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" .
    1.33  
    1.34  lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
    1.35    by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])
    1.36 @@ -486,7 +486,7 @@
    1.37    by transfer (simp add: field_simps)
    1.38  hide_fact (open) compute_float_le
    1.39  
    1.40 -lift_definition is_float_zero :: "float \<Rightarrow> bool"  is "op = 0 :: real \<Rightarrow> bool" by simp
    1.41 +lift_definition is_float_zero :: "float \<Rightarrow> bool"  is "op = 0 :: real \<Rightarrow> bool" .
    1.42  
    1.43  lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
    1.44    by transfer (auto simp add: is_float_zero_def)
    1.45 @@ -1533,7 +1533,7 @@
    1.46  lemma real_of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)"
    1.47    unfolding nprt_def inf_float_def min_def inf_real_def by auto
    1.48  
    1.49 -lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor by simp
    1.50 +lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor .
    1.51  
    1.52  lemma compute_int_floor_fl[code]:
    1.53    "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"