--- a/src/HOL/HOL.thy Sat May 19 19:08:06 2007 +0200
+++ b/src/HOL/HOL.thy Sat May 19 19:08:42 2007 +0200
@@ -1408,6 +1408,12 @@
lemmas eq_sym_conv = eq_commute
+lemma nnf_simps:
+ "(\<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>(P = Q)) = ((P \<and> \<not> Q) \<or> (\<not>P \<and> Q))"
+ "(\<not> \<not>(P)) = P"
+by blast+
+
subsection {* Basic ML bindings *}
@@ -1521,6 +1527,8 @@
val theI = thm "theI"
val theI' = thm "theI'"
val True_implies_equals = thm "True_implies_equals";
+val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms @ @{thms "nnf_simps"})
+
*}
end