--- a/src/HOL/Groebner_Basis.thy Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Groebner_Basis.thy Mon Dec 07 10:38:04 2015 +0100
@@ -10,9 +10,9 @@
subsection \<open>Groebner Bases\<close>
-lemmas bool_simps = simp_thms(1-34) -- \<open>FIXME move to @{theory HOL}\<close>
+lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to @{theory HOL}\<close>
-lemma nnf_simps: -- \<open>FIXME shadows fact binding in @{theory HOL}\<close>
+lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in @{theory HOL}\<close>
"(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
"(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
"(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"