# HG changeset patch # User webertj # Date 1151939861 -7200 # Node ID 642b16a049dbab2611c4fe45ec48021305ed7145 # Parent 07cf246f76a3c8a9c870c79a3be1095d81f3117c CNF tactic invocations moved into comments diff -r 07cf246f76a3 -r 642b16a049db src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Mon Jul 03 16:25:10 2006 +0200 +++ b/src/HOL/ex/SAT_Examples.thy Mon Jul 03 17:17:41 2006 +0200 @@ -23,23 +23,31 @@ by sat lemma "(a & b) | (c & d) \ (a & b) | (c & d)" +(* apply (tactic {* cnf.cnf_rewrite_tac 1 *}) +*) by sat lemma "(a & b) | (c & d) \ (a & b) | (c & d)" +(* apply (tactic {* cnf.cnfx_rewrite_tac 1 *}) apply (erule exE | erule conjE)+ +*) by satx lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \ (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" +(* apply (tactic {* cnf.cnf_rewrite_tac 1 *}) +*) by sat lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \ (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" +(* apply (tactic {* cnf.cnfx_rewrite_tac 1 *}) apply (erule exE | erule conjE)+ +*) by satx lemma "P=P=P=P=P=P=P=P=P=P"