equal
deleted
inserted
replaced
21 end |
21 end |
22 |
22 |
23 structure Metis_Tactic : METIS_TACTIC = |
23 structure Metis_Tactic : METIS_TACTIC = |
24 struct |
24 struct |
25 |
25 |
26 open ATP_Translate |
26 open ATP_Problem_Generate |
27 open ATP_Reconstruct |
27 open ATP_Proof_Reconstruct |
28 open Metis_Translate |
28 open Metis_Generate |
29 open Metis_Reconstruct |
29 open Metis_Reconstruct |
30 |
30 |
31 val new_skolemizer = |
31 val new_skolemizer = |
32 Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) |
32 Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) |
33 |
33 |