# HG changeset patch # User blanchet # Date 1277278806 -7200 # Node ID 26afa11a1fb20b5e73b95f3d76b5337df14557c5 # Parent 6d9923e8d2083df2ddf0cef855ce07c3b631cea3 killed legacy "neg_clausify" and "clausify" diff -r 6d9923e8d208 -r 26afa11a1fb2 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Tue Jun 22 23:54:16 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Wed Jun 23 09:40:06 2010 +0200 @@ -110,7 +110,6 @@ setup ATP_Systems.setup use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML" use "Tools/Sledgehammer/sledgehammer_isar.ML" -setup Sledgehammer_Isar.setup subsection {* The MESON prover *} diff -r 6d9923e8d208 -r 26afa11a1fb2 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 22 23:54:16 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Jun 23 09:40:06 2010 +0200 @@ -22,11 +22,9 @@ val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list val saturate_skolem_cache: theory -> theory option val auto_saturate_skolem_cache: bool Unsynchronized.ref - (* for emergency use where the Skolem cache causes problems *) val neg_clausify: thm -> thm list val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list list * (string * typ) list - val neg_clausify_tac: Proof.context -> int -> tactic val setup: theory -> theory end; @@ -522,6 +520,7 @@ end; +(* For emergency use where the Skolem cache causes problems. *) val auto_saturate_skolem_cache = Unsynchronized.ref true fun conditionally_saturate_skolem_cache thy = @@ -547,20 +546,6 @@ Subgoal.focus (Variable.set_body false ctxt) n st in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end -(*Conversion of a subgoal to conjecture clauses. Each clause has - leading !!-bound universal variables, to express generality. *) -fun neg_clausify_tac ctxt = - neg_skolemize_tac ctxt THEN' - SUBGOAL (fn (prop, i) => - let val ts = Logic.strip_assums_hyp prop in - EVERY' - [Subgoal.FOCUS - (fn {prems, ...} => - (Method.insert_tac - (map forall_intr_vars (maps neg_clausify prems)) i)) ctxt, - REPEAT_DETERM_N (length ts) o etac thin_rl] i - end); - (** setup **) diff -r 6d9923e8d208 -r 26afa11a1fb2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Jun 22 23:54:16 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jun 23 09:40:06 2010 +0200 @@ -12,7 +12,6 @@ val timeout: int Unsynchronized.ref val full_types: bool Unsynchronized.ref val default_params : theory -> (string * string) list -> params - val setup: theory -> theory end; structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = @@ -25,31 +24,6 @@ open ATP_Systems open Sledgehammer_Fact_Minimizer -(** Proof method used in Isar proofs **) - -val neg_clausify_setup = - Method.setup @{binding neg_clausify} - (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac) - o tap (fn _ => legacy_feature "Old 'neg_clausify' method -- \ - \rerun Sledgehammer to obtain a direct \ - \proof")) - "conversion of goal to negated conjecture clauses (legacy)" - -(** Attribute for converting a theorem into clauses **) - -val parse_clausify_attribute : attribute context_parser = - Scan.lift Parse.nat - >> (fn i => Thm.rule_attribute (fn context => fn th => - let val thy = Context.theory_of context in - Meson.make_meta_clause (nth (cnf_axiom thy th) i) - end)) - -val clausify_setup = - Attrib.setup @{binding clausify} - (parse_clausify_attribute - o tap (fn _ => legacy_feature "Old 'clausify' attribute")) - "conversion of theorem to clauses" - (** Sledgehammer commands **) fun add_to_relevance_override ns : relevance_override = @@ -357,8 +331,4 @@ "set and display the default parameters for Sledgehammer" Keyword.thy_decl parse_sledgehammer_params_command -val setup = - neg_clausify_setup - #> clausify_setup - end;