src/HOL/Tools/sat_solver.ML
changeset 17577 e87bf1d8f17a
parent 17541 6a52083b71c3
child 17581 a50a53081808
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Sep 21 21:01:27 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Sep 21 22:01:09 2005 +0200
     1.3 @@ -511,7 +511,7 @@
     1.4  
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
     1.7 -(* the first installed solver (other than "auto" itself) that does not raise *)
     1.8 +(* the last installed solver (other than "auto" itself) that does not raise  *)
     1.9  (* 'NOT_CONFIGURED'.  (However, the solver may return 'UNKNOWN'.)            *)
    1.10  (* ------------------------------------------------------------------------- *)
    1.11  
    1.12 @@ -564,7 +564,6 @@
    1.13  			(* string list *)
    1.14  			val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace"))
    1.15  				handle _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
    1.16 -			val _ = try File.rm (Path.unpack "resolve_trace")
    1.17  			(* PropLogic.prop_formula -> int *)
    1.18  			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
    1.19  			  | cnf_number_of_clauses _                          = 1