cnf_struct renamed to cnf
authorwebertj
Sat Sep 24 13:54:35 2005 +0200 (2005-09-24)
changeset 17627ff1923b1978b
parent 17626 1c1557f7ae5c
child 17628 f4e2587bc7a5
cnf_struct renamed to cnf
src/HOL/SAT.thy
     1.1 --- a/src/HOL/SAT.thy	Sat Sep 24 13:26:40 2005 +0200
     1.2 +++ b/src/HOL/SAT.thy	Sat Sep 24 13:54:35 2005 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Alwen Tiu, Tjark Weber
     1.5      Copyright   2005
     1.6  
     1.7 -Basic setup for the 'sat' tactic.
     1.8 +Basic setup for the 'sat' and 'satx' tactic.
     1.9  *)
    1.10  
    1.11  header {* Reconstructing external resolution proofs for propositional logic *}
    1.12 @@ -16,8 +16,7 @@
    1.13  
    1.14  begin
    1.15  
    1.16 -(*
    1.17 -ML {* structure sat = SATFunc(structure cnf_struct = cnf); *}
    1.18 +ML {* structure sat = SATFunc(structure cnf = cnf); *}
    1.19  
    1.20  method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
    1.21    "SAT solver"
    1.22 @@ -25,7 +24,7 @@
    1.23  method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
    1.24    "SAT solver (with definitional CNF)"
    1.25  
    1.26 -
    1.27 +(*
    1.28  method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
    1.29    "Transforming hypotheses in a goal into CNF"
    1.30