equal
deleted
inserted
replaced
32 if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else (); |
32 if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else (); |
33 |
33 |
34 fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt); |
34 fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt); |
35 |
35 |
36 (*For generating structured proofs: keep every nth proof line*) |
36 (*For generating structured proofs: keep every nth proof line*) |
37 val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1; |
37 val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" (K 1); |
38 |
38 |
39 (*Indicates whether to include sort information in generated proofs*) |
39 (*Indicates whether to include sort information in generated proofs*) |
40 val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true; |
40 val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" (K true); |
41 |
41 |
42 val setup = modulus_setup #> recon_sorts_setup; |
42 val setup = modulus_setup #> recon_sorts_setup; |
43 |
43 |
44 (**** PARSING OF TSTP FORMAT ****) |
44 (**** PARSING OF TSTP FORMAT ****) |
45 |
45 |