--- a/src/HOL/Hilbert_Choice.thy Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Hilbert_Choice.thy Thu Aug 28 16:58:27 2014 +0200
@@ -110,6 +110,20 @@
by (induct n) auto
qed
+
+subsection {* A skolemization tactic and proof method *}
+
+ML {*
+fun skolem_tac ctxt =
+ Atomize_Elim.atomize_elim_tac ctxt THEN'
+ SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice bchoice}) THEN ALLGOALS (blast_tac ctxt));
+*}
+
+method_setup skolem = {*
+ Scan.succeed (SIMPLE_METHOD' o skolem_tac)
+*} "solve skolemization goals"
+
+
subsection {*Function Inverse*}
lemma inv_def: "inv f = (%y. SOME x. f x = y)"
@@ -918,4 +932,3 @@
ML_file "Tools/choice_specification.ML"
end
-
--- a/src/HOL/Sledgehammer.thy Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Aug 28 16:58:27 2014 +0200
@@ -33,8 +33,4 @@
ML_file "Tools/Sledgehammer/sledgehammer.ML"
ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
-method_setup skolem = {*
- Scan.succeed (SIMPLE_METHOD' o Sledgehammer_Proof_Methods.skolem_tac)
-*} "solve skolemization goals"
-
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Aug 28 16:58:27 2014 +0200
@@ -32,7 +32,6 @@
type one_line_params =
((string * stature) list * (proof_method * play_outcome)) * string * int * int
- val skolem_tac : Proof.context -> int -> tactic
val is_proof_method_direct : proof_method -> bool
val string_of_proof_method : Proof.context -> string list -> proof_method -> string
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
@@ -49,10 +48,6 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
-fun skolem_tac ctxt =
- TRY o Atomize_Elim.atomize_elim_tac ctxt THEN'
- SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice}) THEN ALLGOALS (blast_tac ctxt))
-
datatype proof_method =
Metis_Method of string option * string option |
Meson_Method |