Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/positivstellensatz.ML
changeset 63667 24126c564d8a
parent 63648 f9f3006a5579
child 67091 1393c2340eec 
--- 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) =
isabelle