preliminary fix of HOL build problem
authorobua
Sat Sep 24 13:11:05 2005 +0200 (2005-09-24)
changeset 176251539d18e3e9f
parent 17624 da9a5efecde7
child 17626 1c1557f7ae5c
preliminary fix of HOL build problem
src/HOL/SAT.thy
     1.1 --- a/src/HOL/SAT.thy	Sat Sep 24 10:47:22 2005 +0200
     1.2 +++ b/src/HOL/SAT.thy	Sat Sep 24 13:11:05 2005 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  
     1.5  begin
     1.6  
     1.7 +(*
     1.8  ML {* structure sat = SATFunc(structure cnf_struct = cnf); *}
     1.9  
    1.10  method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
    1.11 @@ -24,7 +25,7 @@
    1.12  method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
    1.13    "SAT solver (with definitional CNF)"
    1.14  
    1.15 -(*
    1.16 +
    1.17  method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
    1.18    "Transforming hypotheses in a goal into CNF"
    1.19