# HG changeset patch
# User webertj
# Date 1127562875 -7200
# Node ID ff1923b1978b4800ae35832e8adeaff751f7747b
# Parent  1c1557f7ae5cbb4f0796b05d99cd146b75b338a3
cnf_struct renamed to cnf

diff -r 1c1557f7ae5c -r ff1923b1978b src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Sat Sep 24 13:26:40 2005 +0200
+++ b/src/HOL/SAT.thy	Sat Sep 24 13:54:35 2005 +0200
@@ -3,7 +3,7 @@
     Author:     Alwen Tiu, Tjark Weber
     Copyright   2005
 
-Basic setup for the 'sat' tactic.
+Basic setup for the 'sat' and 'satx' tactic.
 *)
 
 header {* Reconstructing external resolution proofs for propositional logic *}
@@ -16,8 +16,7 @@
 
 begin
 
-(*
-ML {* structure sat = SATFunc(structure cnf_struct = cnf); *}
+ML {* structure sat = SATFunc(structure cnf = cnf); *}
 
 method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
   "SAT solver"
@@ -25,7 +24,7 @@
 method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
   "SAT solver (with definitional CNF)"
 
-
+(*
 method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
   "Transforming hypotheses in a goal into CNF"