--- a/src/HOL/OrderedGroup.thy Mon Apr 10 14:37:23 2006 +0200
+++ b/src/HOL/OrderedGroup.thy Mon Apr 10 16:00:34 2006 +0200
@@ -854,6 +854,12 @@
lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
by (simp add: le_def_meet nprt_def meet_aci)
+lemma pprt_neg: "pprt (-x) = - nprt x"
+ by (simp add: pprt_def nprt_def)
+
+lemma nprt_neg: "nprt (-x) = - pprt x"
+ by (simp add: pprt_def nprt_def)
+
lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
by (simp)
@@ -1029,6 +1035,8 @@
declare diff_le_0_iff_le [simp]
+
+
ML {*
val add_zero_left = thm"add_0";
val add_zero_right = thm"add_0_right";