src/HOL/Groebner_Basis.thy
changeset 61799 4cf66f21b764
parent 61476 1884c40f1539
child 64246 15d1ee6e847b
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -10,9 +10,9 @@
     1.4  
     1.5  subsection \<open>Groebner Bases\<close>
     1.6  
     1.7 -lemmas bool_simps = simp_thms(1-34) -- \<open>FIXME move to @{theory HOL}\<close>
     1.8 +lemmas bool_simps = simp_thms(1-34) \<comment> \<open>FIXME move to @{theory HOL}\<close>
     1.9  
    1.10 -lemma nnf_simps: -- \<open>FIXME shadows fact binding in @{theory HOL}\<close>
    1.11 +lemma nnf_simps: \<comment> \<open>FIXME shadows fact binding in @{theory HOL}\<close>
    1.12    "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
    1.13    "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
    1.14    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"