Lines Matching defs:Proof
6 structure Proof :> Proof =
139 handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err);
195 raise Bug ("Proof.recontructSubst: shouldn't fail:\n" ^ err);
215 raise Bug ("Proof.recontructResolvant: shouldn't fail:\n" ^ err);
221 val () = Print.trace LiteralSet.pp "Proof.reconstructEquality: cl" cl
272 "Proof.reconstructEquality: candidates" candidates
281 raise Bug ("Proof.recontructEquality: shouldn't fail:\n" ^ err);
309 val () = Print.trace Thm.pp "Proof.thmToInference: th" th
318 val () = Print.trace ppThmInf "Proof.thmToInference: thmInf" thmInf
324 val () = Print.trace ppInference "Proof.thmToInference: inf" inf
335 ("Proof.thmToInference: bad inference reconstruction:" ^
346 raise Bug ("Proof.thmToInference: shouldn't fail:\n" ^ err);
395 val () = Print.trace Print.ppInt "Proof.proof: unnecessary clauses" (LiteralSetMap.size ths)
404 val () = Print.trace Thm.pp "Proof.proof: th" th
409 val () = Print.trace Print.ppInt "Proof.proof: size" (length infs)