--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 10:50:30 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:11 2014 +0200
@@ -47,14 +47,17 @@
val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
val e_skolemize_rule = "skolemize"
+val leo2_extcnf_combined_rule = "extcnf_combined"
val spass_pirate_datatype_rule = "DT"
val vampire_skolemisation_rule = "skolemisation"
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
val z3_skolemize_rule = "sk"
val z3_th_lemma_rule = "th-lemma"
+val zipperposition_cnf_rule = "cnf"
val skolemize_rules =
- [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
+ [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
+zipperposition_cnf_rule, leo2_extcnf_combined_rule]
val is_skolemize_rule = member (op =) skolemize_rules
val is_arith_rule = String.isPrefix z3_th_lemma_rule