src/HOL/ex/SAT_Examples.thy
changeset 51337 1012626af0bc
parent 47432 e1576d13e933
child 52059 2f970c7f722b
equal deleted inserted replaced
51336:6c06b8de72f9 51337:1012626af0bc
   533     | and_to_list fm acc = rev (fm :: acc)
   533     | and_to_list fm acc = rev (fm :: acc)
   534   val clauses = and_to_list prop_fm []
   534   val clauses = and_to_list prop_fm []
   535   val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
   535   val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
   536   val cterms = map (Thm.cterm_of @{theory}) terms
   536   val cterms = map (Thm.cterm_of @{theory}) terms
   537   val start = Timing.start ()
   537   val start = Timing.start ()
   538   val thm = sat.rawsat_thm @{context} cterms
   538   val _ = sat.rawsat_thm @{context} cterms
   539 in
   539 in
   540   (Timing.result start, ! sat.counter)
   540   (Timing.result start, ! sat.counter)
   541 end;
   541 end;
   542 *}
   542 *}
   543 
   543