--- a/src/HOL/Library/positivstellensatz.ML Fri Feb 05 14:33:31 2010 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Fri Feb 05 14:33:50 2010 +0100
@@ -275,7 +275,7 @@
"((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))"
by auto};
-val abs_split' = @{lemma "P (abs (x::'a::ordered_idom)) == (x >= 0 & P x | x < 0 & P (-x))"
+val abs_split' = @{lemma "P (abs (x::'a::linordered_idom)) == (x >= 0 & P x | x < 0 & P (-x))"
by (atomize (full)) (auto split add: abs_split)};
val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)"