ProgTutorial/Recipes/Sat.thy
changeset 329 5dffcab68680
parent 294 ee9d53fbb56b
child 346 0fea8b7a14a1
equal deleted inserted replaced
328:c0cae24b9d46 329:5dffcab68680
     1 
     1 
     2 theory Sat
     2 theory Sat
     3 imports Main "../Base"
     3 imports Main "../FirstSteps"
     4 begin
     4 begin
     5 
     5 
     6 section {* SAT Solvers\label{rec:sat} *}
     6 section {* SAT Solvers\label{rec:sat} *}
     7 
     7 
     8 text {*
     8 text {*
    57 text {*
    57 text {*
    58   returns @{ML "BoolVar 1" in PropLogic} for  @{ML pform'} and the table 
    58   returns @{ML "BoolVar 1" in PropLogic} for  @{ML pform'} and the table 
    59   @{ML table'} is:
    59   @{ML table'} is:
    60 
    60 
    61   @{ML_response_fake [display,gray]
    61   @{ML_response_fake [display,gray]
    62   "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"
    62   "map (apfst (string_of_term @{context})) (Termtab.dest table')"
    63   "(\<forall>x. P x, 1)"}
    63   "(\<forall>x. P x, 1)"}
    64   
    64   
    65   In the print out of the tabel, we used some pretty printing scaffolding 
    65   In the print out of the tabel, we used some pretty printing scaffolding 
    66   to see better which assignment the table contains.
    66   to see better which assignment the table contains.
    67  
    67