src/HOL/Library/positivstellensatz.ML
changeset 63648 f9f3006a5579
parent 63211 0bec0d1d9998
child 63667 24126c564d8a
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Aug 09 23:29:54 2016 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Aug 10 09:33:54 2016 +0200
     1.3 @@ -266,7 +266,7 @@
     1.4    by auto};
     1.5  
     1.6  val abs_split' = @{lemma "P \<bar>x::'a::linordered_idom\<bar> == (x >= 0 & P x | x < 0 & P (-x))"
     1.7 -  by (atomize (full)) (auto split add: abs_split)};
     1.8 +  by (atomize (full)) (auto split: abs_split)};
     1.9  
    1.10  val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)"
    1.11    by (atomize (full)) (cases "x <= y", auto simp add: max_def)};