src/HOL/Library/positivstellensatz.ML
changeset 35028 108662d50512
parent 33443 b9bbd0f3dcdb
child 35408 b48ab741683b
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -275,7 +275,7 @@
     1.4    "((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))"
     1.5    by auto};
     1.6  
     1.7 -val abs_split' = @{lemma "P (abs (x::'a::ordered_idom)) == (x >= 0 & P x | x < 0 & P (-x))"
     1.8 +val abs_split' = @{lemma "P (abs (x::'a::linordered_idom)) == (x >= 0 & P x | x < 0 & P (-x))"
     1.9    by (atomize (full)) (auto split add: abs_split)};
    1.10  
    1.11  val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)"