changeset 74117 | 30ab39ab4117 |
parent 74109 | ed1f576df9c4 |
child 74206 | 9c6159cbf9ee |
74116:5cd8b5cd0451 | 74117:30ab39ab4117 |
---|---|
679 if is_format_higher_order format then keep_lamsN |
679 if is_format_higher_order format then keep_lamsN |
680 else combsN, uncurried_aliases), ""))], |
680 else combsN, uncurried_aliases), ""))], |
681 best_max_mono_iters = default_max_mono_iters, |
681 best_max_mono_iters = default_max_mono_iters, |
682 best_max_new_mono_instances = default_max_new_mono_instances} |
682 best_max_new_mono_instances = default_max_new_mono_instances} |
683 |
683 |
684 |
|
685 val dummy_fof_format = FOF |
|
686 val dummy_fof_config = dummy_config Hypothesis dummy_fof_format "mono_guards??" false |
|
687 val dummy_fof = (dummy_fofN, fn () => dummy_fof_config) |
|
688 |
|
684 val dummy_tfx_format = TFF (With_FOOL, Polymorphic) |
689 val dummy_tfx_format = TFF (With_FOOL, Polymorphic) |
685 val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false |
690 val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false |
686 val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config) |
691 val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config) |
687 |
692 |
688 val dummy_thf_format = THF (With_FOOL, Polymorphic, THF_With_Choice) |
693 val dummy_thf_format = THF (With_FOOL, Polymorphic, THF_With_Choice) |
723 end |
728 end |
724 |
729 |
725 val atps = |
730 val atps = |
726 [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, |
731 [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, |
727 remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, |
732 remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, |
728 remote_waldmeister, remote_zipperposition, dummy_tfx, dummy_thf] |
733 remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf] |
729 |
734 |
730 val _ = Theory.setup (fold add_atp atps) |
735 val _ = Theory.setup (fold add_atp atps) |
731 |
736 |
732 end; |
737 end; |