Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned whitespace;
authorwenzelm
Thu, 11 Aug 2016 15:36:17 +0200
changeset 63667 24126c564d8a
parent 63666 ff6caffcaed4
child 63668 5efaa884ac6c
tuned whitespace;
src/HOL/Library/positivstellensatz.ML file | annotate | diff | comparison | revisions 
--- 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