author blanchet Thu, 24 Jun 2010 17:57:36 +0200 changeset 37541 a76ace919f1c parent 37540 48273d1ea331 child 37542 8db1e5d4b93f
never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
```--- a/src/HOL/Sledgehammer.thy	Thu Jun 24 17:27:18 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Jun 24 17:57:36 2010 +0200
@@ -53,16 +53,6 @@
lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"

-text{*These two represent the equivalence between Boolean equality and iff.
-They can't be converted to clauses automatically, as the iff would be
-expanded...*}
-
-lemma iff_positive: "P \<or> Q \<or> P = Q"
-by blast
-
-lemma iff_negative: "\<not> P \<or> \<not> Q \<or> P = Q"
-by blast
-
text{*Theorems for translation to combinators*}

lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 17:27:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 24 17:57:36 2010 +0200
@@ -35,13 +35,15 @@

type cnf_thm = thm * ((string * int) * thm)

+val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+
(* Used to label theorems chained into the goal. *)
-val chained_prefix = "Sledgehammer.chained_"
+val chained_prefix = sledgehammer_prefix ^ "chained_"

val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();

-val skolem_theory_name = "Sledgehammer.Sko"
+val skolem_theory_name = sledgehammer_prefix ^ "Sko"
val skolem_prefix = "sko_"
val skolem_infix = "\$"

@@ -382,6 +384,8 @@