equal
deleted
inserted
replaced
25 end; |
25 end; |
26 |
26 |
27 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = |
27 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = |
28 struct |
28 struct |
29 |
29 |
|
30 open Clausifier |
30 open Sledgehammer_Util |
31 open Sledgehammer_Util |
31 open Sledgehammer_FOL_Clause |
32 open Sledgehammer_FOL_Clause |
32 open Sledgehammer_HOL_Clause |
33 open Sledgehammer_HOL_Clause |
33 open Sledgehammer_Fact_Preprocessor |
|
34 |
34 |
35 type minimize_command = string list -> string |
35 type minimize_command = string list -> string |
36 |
36 |
37 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" |
37 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" |
38 fun is_head_digit s = Char.isDigit (String.sub (s, 0)) |
38 fun is_head_digit s = Char.isDigit (String.sub (s, 0)) |