src/HOL/Tools/sat_funcs.ML
 changeset 20486 02ca20e33030 parent 20464 2b3fc1459ffa child 21267 5294ecae6708
equal inserted replaced
20485:3078fd2eec7b 20486:02ca20e33030
`   313 		else`
`   313 		else`
`   314 			let`
`   314 			let`
`   315 				(* optimization: convert the given clauses from "[c_i] |- c_i" to *)`
`   315 				(* optimization: convert the given clauses from "[c_i] |- c_i" to *)`
`   316 				(* "[c_1 && ... && c_n] |- c_i"; this avoids accumulation of      *)`
`   316 				(* "[c_1 && ... && c_n] |- c_i"; this avoids accumulation of      *)`
`   317 				(* hypotheses during resolution                                   *)`
`   317 				(* hypotheses during resolution                                   *)`
`   321 				(* [c_1 && ... && c_n] |- c_1 && ... && c_n *)`
`   318 				(* [c_1 && ... && c_n] |- c_1 && ... && c_n *)`
`   322 				val cnf_cterm = mk_conjunction_list (map cprop_of non_triv_clauses)`
`   319 				val cnf_cterm = Conjunction.mk_conjunction_list (map cprop_of non_triv_clauses)`
`   323 				val cnf_thm   = Thm.assume cnf_cterm`
`   320 				val cnf_thm   = Thm.assume cnf_cterm`
`   324 				(* cf. Conjunction.elim_list *)`
`   321 				(* cf. Conjunction.elim_list *)`
`   325 				fun right_elim_list th =`
`   322 				fun right_elim_list th =`
`   326 					let val (th1, th2) = Conjunction.elim th`
`   323 					let val (th1, th2) = Conjunction.elim th`
`   327 					in th1 :: right_elim_list th2 end handle THM _ => [th]`
`   324 					in th1 :: right_elim_list th2 end handle THM _ => [th]`