src/HOL/OrderedGroup.thy
changeset 19404 9bf2cdc9e8e8
parent 19233 77ca20b0ed77
child 19527 9b5c38e8e780
     1.1 --- a/src/HOL/OrderedGroup.thy	Mon Apr 10 14:37:23 2006 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Mon Apr 10 16:00:34 2006 +0200
     1.3 @@ -854,6 +854,12 @@
     1.4  lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
     1.5    by (simp add: le_def_meet nprt_def meet_aci)
     1.6  
     1.7 +lemma pprt_neg: "pprt (-x) = - nprt x"
     1.8 +  by (simp add: pprt_def nprt_def)
     1.9 +
    1.10 +lemma nprt_neg: "nprt (-x) = - pprt x"
    1.11 +  by (simp add: pprt_def nprt_def)
    1.12 +
    1.13  lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
    1.14  by (simp)
    1.15  
    1.16 @@ -1029,6 +1035,8 @@
    1.17  declare diff_le_0_iff_le [simp]
    1.18  
    1.19  
    1.20 +
    1.21 +
    1.22  ML {*
    1.23  val add_zero_left = thm"add_0";
    1.24  val add_zero_right = thm"add_0_right";