# HG changeset patch
# User webertj
# Date 1183735278 -7200
# Node ID 451ab1a20ac35c7bcf1966de0f54f133606b95ee
# Parent  e65e36dbe0d2fcbcc2bb7c42099373d7c887e558
cosmetic (line length fixed)

diff -r e65e36dbe0d2 -r 451ab1a20ac3 src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Fri Jul 06 16:09:28 2007 +0200
+++ b/src/HOL/ex/SAT_Examples.thy	Fri Jul 06 17:21:18 2007 +0200
@@ -37,15 +37,15 @@
 *)
 by satx
 
-lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow>
-  (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
+lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
+  \<Longrightarrow> (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) \<Longrightarrow>
-  (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
+lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
+  \<Longrightarrow> (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)+
@@ -82,7 +82,8 @@
 ML {* reset sat.trace_sat; *}
 ML {* reset quick_and_dirty; *}
 
-method_setup rawsat = {* Method.no_args (Method.SIMPLE_METHOD' sat.rawsat_tac) *}
+method_setup rawsat =
+  {* Method.no_args (Method.SIMPLE_METHOD' sat.rawsat_tac) *}
   "SAT solver (no preprocessing)"
 
 (* ML {* Toplevel.profiling := 1; *} *)
@@ -513,15 +514,21 @@
 by rawsat  -- {* this is without CNF conversion *}
 
 (* Old sequent clause representation ("[c_i, p, ~q, \<dots>] \<turnstile> False"):
-   sat, zchaff_with_proofs: 8705 resolution steps in +++ User 1.154  All 1.189 secs
-   sat, minisat_with_proofs: 40790 resolution steps in +++ User 3.762  All 3.806 secs
+   sat, zchaff_with_proofs: 8705 resolution steps in
+                            +++ User 1.154  All 1.189 secs
+   sat, minisat_with_proofs: 40790 resolution steps in
+                             +++ User 3.762  All 3.806 secs
 
-   rawsat, zchaff_with_proofs: 8705 resolution steps in +++ User 0.731  All 0.751 secs
-   rawsat, minisat_with_proofs: 40790 resolution steps in +++ User 3.514  All 3.550 secs
+   rawsat, zchaff_with_proofs: 8705 resolution steps in
+                               +++ User 0.731  All 0.751 secs
+   rawsat, minisat_with_proofs: 40790 resolution steps in
+                                +++ User 3.514  All 3.550 secs
 
    CNF clause representation ("[c_1 && \<dots> && c_n, p, ~q, \<dots>] \<turnstile> False"):
-   rawsat, zchaff_with_proofs: 8705 resolution steps in +++ User 0.653  All 0.670 secs
-   rawsat, minisat_with_proofs: 40790 resolution steps in +++ User 1.860  All 1.886 secs
+   rawsat, zchaff_with_proofs: 8705 resolution steps in
+                               +++ User 0.653  All 0.670 secs
+   rawsat, minisat_with_proofs: 40790 resolution steps in
+                                +++ User 1.860  All 1.886 secs
 
    (as of 2006-08-30, on a 2.5 GHz Pentium 4)
 *)