Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
authorblanchet
Thu, 24 Jul 2014 18:46:38 +0200
changeset 57654 f89c0749533d
parent 57653 4b247a7586c9
child 57655 dde0e76996ad
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 24 17:58:29 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 24 18:46:38 2014 +0200
@@ -46,7 +46,7 @@
 
 val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
 
-val e_skolemize_rules = ["skolemize", "shift_quantors"]
+val e_skolemize_rule = "skolemize"
 val spass_pirate_datatype_rule = "DT"
 val vampire_skolemisation_rule = "skolemisation"
 (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
@@ -54,7 +54,7 @@
 val z3_th_lemma_rule = "th-lemma"
 
 val skolemize_rules =
-  e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
+  [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
 
 val is_skolemize_rule = member (op =) skolemize_rules
 val is_arith_rule = String.isPrefix z3_th_lemma_rule
isabelle