equal
deleted
inserted
replaced
26 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = |
26 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = |
27 struct |
27 struct |
28 |
28 |
29 open ATP_Util |
29 open ATP_Util |
30 open ATP_Problem |
30 open ATP_Problem |
|
31 open ATP_Problem_Generate |
31 open ATP_Proof |
32 open ATP_Proof |
32 open ATP_Proof_Reconstruct |
33 open ATP_Proof_Reconstruct |
33 open ATP_Waldmeister |
|
34 open Sledgehammer_Util |
34 open Sledgehammer_Util |
35 open Sledgehammer_Proof_Methods |
35 open Sledgehammer_Proof_Methods |
36 open Sledgehammer_Isar_Proof |
36 open Sledgehammer_Isar_Proof |
37 open Sledgehammer_Isar_Preplay |
37 open Sledgehammer_Isar_Preplay |
38 open Sledgehammer_Isar_Compress |
38 open Sledgehammer_Isar_Compress |
60 val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") |
60 val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") |
61 val zipperposition_cnf_rule = "cnf" |
61 val zipperposition_cnf_rule = "cnf" |
62 |
62 |
63 val skolemize_rules = |
63 val skolemize_rules = |
64 [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, |
64 [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, |
65 spass_skolemize_rule, vampire_skolemisation_rule, |
65 spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule, |
66 veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule] |
66 zipperposition_cnf_rule] |
67 |
67 |
68 fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule) |
68 fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule) |
69 val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix |
69 val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix |
70 |
70 |
71 val is_skolemize_rule = member (op =) skolemize_rules |
71 val is_skolemize_rule = member (op =) skolemize_rules |