equal
deleted
inserted
replaced
36 val trace_path = Path.basic "atp_trace"; |
36 val trace_path = Path.basic "atp_trace"; |
37 |
37 |
38 fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s |
38 fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s |
39 else (); |
39 else (); |
40 |
40 |
41 val string_of_thm = PrintMode.setmp [] string_of_thm; |
41 val string_of_thm = PrintMode.setmp [] Display.string_of_thm; |
42 |
42 |
43 (*For generating structured proofs: keep every nth proof line*) |
43 (*For generating structured proofs: keep every nth proof line*) |
44 val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1; |
44 val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1; |
45 |
45 |
46 (*Indicates whether to include sort information in generated proofs*) |
46 (*Indicates whether to include sort information in generated proofs*) |