# HG changeset patch
# User fleury
# Date 1406721791 -7200
# Node ID dfc834e39c1f4059e6cdac599ea957fb05abe53a
# Parent  13b446b628252972785479cb31d14fe49e53b954
Skolemization support for leo-II and Zipperposition.

diff -r 13b446b62825 -r dfc834e39c1f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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