src/HOL/Library/positivstellensatz.ML
changeset 63667 24126c564d8a
parent 63648 f9f3006a5579
child 67091 1393c2340eec
equal deleted inserted replaced
63666:ff6caffcaed4 63667:24126c564d8a
   493     fun equal_implies_1_rule PQ =
   493     fun equal_implies_1_rule PQ =
   494       let
   494       let
   495         val P = Thm.lhs_of PQ
   495         val P = Thm.lhs_of PQ
   496       in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
   496       in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
   497       end
   497       end
   498     (* FIXME!!! Copied from groebner.ml *)
   498     (*FIXME!!! Copied from groebner.ml*)
   499     val strip_exists =
   499     val strip_exists =
   500       let
   500       let
   501         fun h (acc, t) =
   501         fun h (acc, t) =
   502           case Thm.term_of t of
   502           case Thm.term_of t of
   503             Const(@{const_name Ex},_)$Abs(_,_,_) =>
   503             Const(@{const_name Ex},_)$Abs(_,_,_) =>