src/HOL/Int.thy
changeset 67969 83c8cafdebe8
parent 67399 eab6ce8368fa
child 68721 53ad5c01be3f
     1.1 --- a/src/HOL/Int.thy	Sun Apr 08 12:31:08 2018 +0200
     1.2 +++ b/src/HOL/Int.thy	Mon Apr 09 15:20:11 2018 +0100
     1.3 @@ -111,7 +111,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -
     1.8  subsection \<open>Ordering properties of arithmetic operations\<close>
     1.9  
    1.10  instance int :: ordered_cancel_ab_semigroup_add
    1.11 @@ -423,6 +422,12 @@
    1.12  lemma of_int_power_less_of_int_cancel_iff[simp]: "of_int x < (of_int b) ^ w\<longleftrightarrow> x < b ^ w"
    1.13    by (metis (mono_tags) of_int_less_iff of_int_power)
    1.14  
    1.15 +lemma of_int_max: "of_int (max x y) = max (of_int x) (of_int y)"
    1.16 +  by (auto simp: max_def)
    1.17 +
    1.18 +lemma of_int_min: "of_int (min x y) = min (of_int x) (of_int y)"
    1.19 +  by (auto simp: min_def)
    1.20 +
    1.21  end
    1.22  
    1.23  text \<open>Comparisons involving @{term of_int}.\<close>