# HG changeset patch
# User wenzelm
# Date 1470922577 -7200
# Node ID 24126c564d8adf11d9f92a6e9dd966f22152278b
# Parent  ff6caffcaed46481a1c0b1c763cd2e44d4054dcd
tuned whitespace;

diff -r ff6caffcaed4 -r 24126c564d8a src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Thu Aug 11 15:32:53 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Thu Aug 11 15:36:17 2016 +0200
@@ -495,7 +495,7 @@
         val P = Thm.lhs_of PQ
       in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
       end
-    (* FIXME!!! Copied from groebner.ml *)
+    (*FIXME!!! Copied from groebner.ml*)
     val strip_exists =
       let
         fun h (acc, t) =