src/HOL/Library/positivstellensatz.ML
changeset 63667 24126c564d8a
parent 63648 f9f3006a5579
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Aug 11 15:32:53 2016 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Aug 11 15:36:17 2016 +0200
     1.3 @@ -495,7 +495,7 @@
     1.4          val P = Thm.lhs_of PQ
     1.5        in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
     1.6        end
     1.7 -    (* FIXME!!! Copied from groebner.ml *)
     1.8 +    (*FIXME!!! Copied from groebner.ml*)
     1.9      val strip_exists =
    1.10        let
    1.11          fun h (acc, t) =