src/HOL/Imperative_HOL/ex/SatChecker.thy
changeset 37826 4c0a5e35931a
parent 37806 a7679be14442
child 40671 5e46057ba8e0
equal deleted inserted replaced
37825:adc1143bc1a8 37826:4c0a5e35931a
   708   (SML "MinisatProofStep.ProofStep")
   708   (SML "MinisatProofStep.ProofStep")
   709 
   709 
   710 code_const ProofDone  and  Root              and  Conflict              and  Delete  and  Xstep
   710 code_const ProofDone  and  Root              and  Conflict              and  Delete  and  Xstep
   711      (SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))")
   711      (SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))")
   712 
   712 
   713 export_code checker in SML module_name SAT file -
   713 export_code checker tchecker lchecker in SML
   714 export_code tchecker in SML module_name SAT file -
       
   715 export_code lchecker in SML module_name SAT file -
       
   716 
   714 
   717 end
   715 end