# HG changeset patch
# User blanchet
# Date 1302773045 -7200
# Node ID 128dc0fa87fc1077336ba3beb730a360fadbc4b1
# Parent  721e85fd2db3aa4246139299d5cc17e67ea31705
more clausification tests

diff -r 721e85fd2db3 -r 128dc0fa87fc src/HOL/Metis_Examples/Clausify.thy
--- a/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:05 2011 +0200
+++ b/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:05 2011 +0200
@@ -71,6 +71,18 @@
 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
 by (metisFT rax)
 
+lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
+       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
+       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
+       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
+by (metis rax)
+
+lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
+       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
+       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
+       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
+by (metisFT rax)
+
 text {* Definitional CNF for goal *}
 
 axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where