equal
deleted
inserted
replaced
6 struct |
6 struct |
7 |
7 |
8 val proverK = "prover" |
8 val proverK = "prover" |
9 val prover_timeoutK = "prover_timeout" |
9 val prover_timeoutK = "prover_timeout" |
10 val keepK = "keep" |
10 val keepK = "keep" |
11 val full_typesK = "full_types" |
|
12 val type_sysK = "type_sys" |
11 val type_sysK = "type_sys" |
13 val slicingK = "slicing" |
12 val slicingK = "slicing" |
14 val e_weight_methodK = "e_weight_method" |
13 val e_weight_methodK = "e_weight_method" |
15 val spass_force_sosK = "spass_force_sos" |
14 val spass_force_sosK = "spass_force_sos" |
16 val vampire_force_sosK = "vampire_force_sos" |
15 val vampire_force_sosK = "vampire_force_sos" |
628 else () |
627 else () |
629 end |
628 end |
630 end |
629 end |
631 |
630 |
632 fun invoke args = |
631 fun invoke args = |
633 let |
632 Mirabelle.register (init, sledgehammer_action args, done) |
634 val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK |
|
635 in Mirabelle.register (init, sledgehammer_action args, done) end |
|
636 |
633 |
637 end |
634 end |