# HG changeset patch
# User huffman
# Date 1314108725 25200
# Node ID aae9c9a0735e8161355a746d9e8ce282488a4e68
# Parent  8382f4c2470c5d1bba95f93ccf65e4061fb292a4# Parent  f74707e12d30348eda0e014a1ba64c7ccc02cb66
merged

diff -r 8382f4c2470c -r aae9c9a0735e doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Mon Aug 22 18:15:33 2011 -0700
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Tue Aug 23 07:12:05 2011 -0700
@@ -176,14 +176,14 @@
 set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
 \texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
-with E 1.0 to 1.3, SPASS 3.5 and 3.7, and Vampire 0.6 and 1.0%
+with E 1.0 to 1.3, SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
 \footnote{Following the rewrite of Vampire, the counter for version numbers was
-reset to 0; hence the (new) Vampire versions 0.6 and 1.0 are more recent than,
-say, Vampire 11.5.}%
+reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
+than, say, Vampire 9.0 or 11.5.}%
 . Since the ATPs' output formats are neither documented nor stable, other
 versions of the ATPs might or might not work well with Sledgehammer. Ideally,
 also set \texttt{E\_VERSION}, \texttt{SPASS\_VERSION}, or
-\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.3'').
+\texttt{VAMPIRE\_VERSION} to the ATP's version number (e.g., ``1.4'').
 \end{enum}
 
 To check whether E and SPASS are successfully installed, follow the example in
@@ -750,7 +750,9 @@
 prover developed by Andrei Voronkov and his colleagues
 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
-executable. Sledgehammer has been tested with versions 11, 0.6, and 1.0.
+executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').
+Sledgehammer has been tested with versions 0.6, 1.0, and 1.8. Vampire 1.8
+supports the TPTP many-typed first-order format (TFF).
 
 \item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
 SRI \cite{yices}. To use Yices, set the environment variable
@@ -760,12 +762,13 @@
 \item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
 Microsoft Research \cite{z3}. To use Z3, set the environment variable
 \texttt{Z3\_SOLVER} to the complete path of the executable, including the file
-name, and set \texttt{Z3\_NON\_COMMERCIAL=yes} to confirm that you are a
+name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
 noncommercial user. Sledgehammer has been tested with versions 2.7 to 2.18.
 
-\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
-ATP, exploiting Z3's undocumented support for the TPTP format. It is included
-for experimental purposes. It requires version 2.18 or above.
+\item[$\bullet$] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
+an ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order
+formats (FOF and TFF). It is included for experimental purposes. It requires
+version 3.0 or above.
 \end{enum}
 
 In addition, the following remote provers are supported:
@@ -799,7 +802,7 @@
 Geoff Sutcliffe's Miami servers.
 
 \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
-Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
+Vampire runs on Geoff Sutcliffe's Miami servers. Version 1.8 is used.
 
 \item[$\bullet$] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
 equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
@@ -811,8 +814,8 @@
 servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
 point).
 
-\item[$\bullet$] \textbf{\textit{remote\_z3\_atp}:} The remote version of ``Z3
-as an ATP'' runs on Geoff Sutcliffe's Miami servers.
+\item[$\bullet$] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
+with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
 By default, Sledgehammer will run E, E-SInE, SPASS, Vampire, Z3 (or whatever
diff -r 8382f4c2470c -r aae9c9a0735e src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Aug 22 18:15:33 2011 -0700
+++ b/src/HOL/Predicate.thy	Tue Aug 23 07:12:05 2011 -0700
@@ -47,7 +47,7 @@
   done
 
 lemma rev_predicate1D:
-  "P x ==> P <= Q ==> Q x"
+  "P x \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x"
   by (rule predicate1D)
 
 lemma predicate2I [Pure.intro!, intro!]:
@@ -67,100 +67,100 @@
   done
 
 lemma rev_predicate2D:
-  "P x y ==> P <= Q ==> Q x y"
+  "P x y \<Longrightarrow> P \<le> Q \<Longrightarrow> Q x y"
   by (rule predicate2D)
 
 
 subsubsection {* Equality *}
 
-lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
-  by (simp add: mem_def)
+lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
+  by (simp add: set_eq_iff fun_eq_iff mem_def)
 
-lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
-  by (simp add: fun_eq_iff mem_def)
+lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
+  by (simp add: set_eq_iff fun_eq_iff mem_def)
 
 
 subsubsection {* Order relation *}
 
-lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
-  by (simp add: mem_def)
+lemma pred_subset_eq: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
+  by (simp add: subset_iff le_fun_def mem_def)
 
-lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) <= (\<lambda>x y. (x, y) \<in> S)) = (R <= S)"
-  by fast
+lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
+  by (simp add: subset_iff le_fun_def mem_def)
 
 
 subsubsection {* Top and bottom elements *}
 
-lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
+lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P"
   by (simp add: bot_fun_def)
 
-lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
+lemma bot2E [elim!]: "\<bottom> x y \<Longrightarrow> P"
   by (simp add: bot_fun_def)
 
-lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
+lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
   by (auto simp add: fun_eq_iff)
 
-lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
+lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
   by (auto simp add: fun_eq_iff)
 
-lemma top1I [intro!]: "top x"
+lemma top1I [intro!]: "\<top> x"
   by (simp add: top_fun_def)
 
-lemma top2I [intro!]: "top x y"
+lemma top2I [intro!]: "\<top> x y"
   by (simp add: top_fun_def)
 
 
 subsubsection {* Binary intersection *}
 
-lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
+lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
   by (simp add: inf_fun_def)
 
-lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
+lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
   by (simp add: inf_fun_def)
 
-lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
+lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
   by (simp add: inf_fun_def)
 
-lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
+lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
   by (simp add: inf_fun_def)
 
-lemma inf1D1: "inf A B x ==> A x"
+lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
   by (simp add: inf_fun_def)
 
-lemma inf2D1: "inf A B x y ==> A x y"
+lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
   by (simp add: inf_fun_def)
 
-lemma inf1D2: "inf A B x ==> B x"
+lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
   by (simp add: inf_fun_def)
 
-lemma inf2D2: "inf A B x y ==> B x y"
+lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
   by (simp add: inf_fun_def)
 
-lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
+lemma inf_Int_eq: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   by (simp add: inf_fun_def mem_def)
 
-lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
+lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
   by (simp add: inf_fun_def mem_def)
 
 
 subsubsection {* Binary union *}
 
-lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
+lemma sup1I1 [elim?]: "A x \<Longrightarrow> (A \<squnion> B) x"
   by (simp add: sup_fun_def)
 
-lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
+lemma sup2I1 [elim?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
   by (simp add: sup_fun_def)
 
-lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
+lemma sup1I2 [elim?]: "B x \<Longrightarrow> (A \<squnion> B) x"
   by (simp add: sup_fun_def)
 
-lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
+lemma sup2I2 [elim?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
   by (simp add: sup_fun_def)
 
-lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
+lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
   by (simp add: sup_fun_def) iprover
 
-lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
+lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   by (simp add: sup_fun_def) iprover
 
 text {*
@@ -168,76 +168,76 @@
   @{text B}.
 *}
 
-lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
+lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   by (auto simp add: sup_fun_def)
 
-lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
+lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
   by (auto simp add: sup_fun_def)
 
-lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
+lemma sup_Un_eq: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
   by (simp add: sup_fun_def mem_def)
 
-lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
+lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
   by (simp add: sup_fun_def mem_def)
 
 
 subsubsection {* Intersections of families *}
 
-lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
+lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
   by (simp add: INFI_apply)
 
-lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
+lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
   by (simp add: INFI_apply)
 
-lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
+lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
   by (auto simp add: INFI_apply)
 
-lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
+lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
   by (auto simp add: INFI_apply)
 
-lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
+lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
   by (auto simp add: INFI_apply)
 
-lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
+lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
   by (auto simp add: INFI_apply)
 
-lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
+lemma INF1_E [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
   by (auto simp add: INFI_apply)
 
-lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
+lemma INF2_E [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
   by (auto simp add: INFI_apply)
 
-lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
+lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Sqinter>i. r i))"
   by (simp add: INFI_apply fun_eq_iff)
 
-lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
+lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Sqinter>i. r i))"
   by (simp add: INFI_apply fun_eq_iff)
 
 
 subsubsection {* Unions of families *}
 
-lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)"
+lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
   by (simp add: SUPR_apply)
 
-lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
+lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
   by (simp add: SUPR_apply)
 
-lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
+lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
   by (auto simp add: SUPR_apply)
 
-lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
+lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
   by (auto simp add: SUPR_apply)
 
-lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
+lemma SUP1_E [elim!]: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R"
   by (auto simp add: SUPR_apply)
 
-lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
+lemma SUP2_E [elim!]: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R"
   by (auto simp add: SUPR_apply)
 
-lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
+lemma SUP_UN_eq: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   by (simp add: SUPR_apply fun_eq_iff)
 
-lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
+lemma SUP_UN_eq2: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
   by (simp add: SUPR_apply fun_eq_iff)
 
 
@@ -245,12 +245,9 @@
 
 subsubsection {* Composition  *}
 
-inductive
-  pred_comp  :: "['a => 'b => bool, 'b => 'c => bool] => 'a => 'c => bool"
-    (infixr "OO" 75)
-  for r :: "'a => 'b => bool" and s :: "'b => 'c => bool"
-where
-  pred_compI [intro]: "r a b ==> s b c ==> (r OO s) a c"
+inductive pred_comp  :: "['a \<Rightarrow> 'b \<Rightarrow> bool, 'b \<Rightarrow> 'c \<Rightarrow> bool] \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> bool" (infixr "OO" 75)
+  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and s :: "'b \<Rightarrow> 'c \<Rightarrow> bool" where
+  pred_compI [intro]: "r a b \<Longrightarrow> s b c \<Longrightarrow> (r OO s) a c"
 
 inductive_cases pred_compE [elim!]: "(r OO s) a c"
 
@@ -261,12 +258,9 @@
 
 subsubsection {* Converse *}
 
-inductive
-  conversep :: "('a => 'b => bool) => 'b => 'a => bool"
-    ("(_^--1)" [1000] 1000)
-  for r :: "'a => 'b => bool"
-where
-  conversepI: "r a b ==> r^--1 b a"
+inductive conversep :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(_^--1)" [1000] 1000)
+  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+  conversepI: "r a b \<Longrightarrow> r^--1 b a"
 
 notation (xsymbols)
   conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
@@ -290,13 +284,13 @@
   by (iprover intro: order_antisym conversepI pred_compI
     elim: pred_compE dest: conversepD)
 
-lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
+lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1"
   by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
 
-lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
+lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1"
   by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
 
-lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
+lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
   by (auto simp add: fun_eq_iff)
 
 lemma conversep_eq [simp]: "(op =)^--1 = op ="
@@ -305,11 +299,9 @@
 
 subsubsection {* Domain *}
 
-inductive
-  DomainP :: "('a => 'b => bool) => 'a => bool"
-  for r :: "'a => 'b => bool"
-where
-  DomainPI [intro]: "r a b ==> DomainP r a"
+inductive DomainP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+  DomainPI [intro]: "r a b \<Longrightarrow> DomainP r a"
 
 inductive_cases DomainPE [elim!]: "DomainP r a"
 
@@ -319,11 +311,9 @@
 
 subsubsection {* Range *}
 
-inductive
-  RangeP :: "('a => 'b => bool) => 'b => bool"
-  for r :: "'a => 'b => bool"
-where
-  RangePI [intro]: "r a b ==> RangeP r b"
+inductive RangeP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool"
+  for r :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where
+  RangePI [intro]: "r a b \<Longrightarrow> RangeP r b"
 
 inductive_cases RangePE [elim!]: "RangeP r b"
 
@@ -333,9 +323,8 @@
 
 subsubsection {* Inverse image *}
 
-definition
-  inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
-  "inv_imagep r f == %x y. r (f x) (f y)"
+definition inv_imagep :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where
+  "inv_imagep r f = (\<lambda>x y. r (f x) (f y))"
 
 lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
   by (simp add: inv_image_def inv_imagep_def)
@@ -347,7 +336,7 @@
 subsubsection {* Powerset *}
 
 definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
-  "Powp A == \<lambda>B. \<forall>x \<in> B. A x"
+  "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)"
 
 lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
   by (auto simp add: Powp_def fun_eq_iff)
@@ -357,14 +346,14 @@
 
 subsubsection {* Properties of relations *}
 
-abbreviation antisymP :: "('a => 'a => bool) => bool" where
-  "antisymP r == antisym {(x, y). r x y}"
+abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "antisymP r \<equiv> antisym {(x, y). r x y}"
 
-abbreviation transP :: "('a => 'a => bool) => bool" where
-  "transP r == trans {(x, y). r x y}"
+abbreviation transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "transP r \<equiv> trans {(x, y). r x y}"
 
-abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
-  "single_valuedP r == single_valued {(x, y). r x y}"
+abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+  "single_valuedP r \<equiv> single_valued {(x, y). r x y}"
 
 (*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*)
 
@@ -474,17 +463,17 @@
   by (simp add: Sup_pred_def)
 
 instance proof
-qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def)
+qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def le_fun_def less_fun_def)
 
 end
 
 lemma eval_INFI [simp]:
   "eval (INFI A f) = INFI A (eval \<circ> f)"
-  by (unfold INFI_def) simp
+  by (simp only: INFI_def eval_Inf image_compose)
 
 lemma eval_SUPR [simp]:
   "eval (SUPR A f) = SUPR A (eval \<circ> f)"
-  by (unfold SUPR_def) simp
+  by (simp only: SUPR_def eval_Sup image_compose)
 
 instantiation pred :: (type) complete_boolean_algebra
 begin
@@ -504,7 +493,7 @@
   by (simp add: minus_pred_def)
 
 instance proof
-qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply)
+qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply INF_apply SUP_apply)
 
 end
 
@@ -524,7 +513,7 @@
 
 lemma bind_bind:
   "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
-  by (rule pred_eqI) auto
+  by (rule pred_eqI) (auto simp add: SUP_apply)
 
 lemma bind_single:
   "P \<guillemotright>= single = P"
@@ -544,7 +533,7 @@
 
 lemma Sup_bind:
   "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
-  by (rule pred_eqI) auto
+  by (rule pred_eqI) (auto simp add: SUP_apply)
 
 lemma pred_iffI:
   assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
@@ -589,8 +578,7 @@
 lemma not_bot:
   assumes "A \<noteq> \<bottom>"
   obtains x where "eval A x"
-  using assms by (cases A)
-    (auto simp add: bot_pred_def, auto simp add: mem_def)
+  using assms by (cases A) (auto simp add: bot_pred_def, simp add: mem_def)
   
 
 subsubsection {* Emptiness check and definite choice *}
@@ -761,7 +749,7 @@
   assumes "P \<bottom>"
   assumes "P (single ())"
   shows "P Q"
-using assms unfolding bot_pred_def Collect_def empty_def single_def proof (cases Q)
+using assms unfolding bot_pred_def bot_fun_def bot_bool_def empty_def single_def proof (cases Q)
   fix f
   assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))"
   then have "P (Pred f)" 
@@ -790,7 +778,7 @@
 
 lemma eval_map [simp]:
   "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
-  by (auto simp add: map_def)
+  by (auto simp add: map_def comp_def)
 
 enriched_type map: map
   by (rule ext, rule pred_eqI, auto)+
@@ -801,9 +789,9 @@
 datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
 
 primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
-    "pred_of_seq Empty = \<bottom>"
-  | "pred_of_seq (Insert x P) = single x \<squnion> P"
-  | "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"
+  "pred_of_seq Empty = \<bottom>"
+| "pred_of_seq (Insert x P) = single x \<squnion> P"
+| "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq"
 
 definition Seq :: "(unit \<Rightarrow> 'a seq) \<Rightarrow> 'a pred" where
   "Seq f = pred_of_seq (f ())"
@@ -812,8 +800,8 @@
 
 primrec member :: "'a seq \<Rightarrow> 'a \<Rightarrow> bool"  where
   "member Empty x \<longleftrightarrow> False"
-  | "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x"
-  | "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x"
+| "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x"
+| "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x"
 
 lemma eval_member:
   "member xq = eval (pred_of_seq xq)"
@@ -836,9 +824,9 @@
   unfolding Seq_def by simp
 
 primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
-    "apply f Empty = Empty"
-  | "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
-  | "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
+  "apply f Empty = Empty"
+| "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
+| "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
 
 lemma apply_bind:
   "pred_of_seq (apply f xq) = pred_of_seq xq \<guillemotright>= f"
@@ -862,9 +850,9 @@
   unfolding Seq_def by simp
 
 primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where
-    "adjunct P Empty = Join P Empty"
-  | "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)"
-  | "adjunct P (Join Q xq) = Join Q (adjunct P xq)"
+  "adjunct P Empty = Join P Empty"
+| "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)"
+| "adjunct P (Join Q xq) = Join Q (adjunct P xq)"
 
 lemma adjunct_sup:
   "pred_of_seq (adjunct P xq) = P \<squnion> pred_of_seq xq"
@@ -891,13 +879,13 @@
 qed
 
 primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
-    "contained Empty Q \<longleftrightarrow> True"
-  | "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
-  | "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q"
+  "contained Empty Q \<longleftrightarrow> True"
+| "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q"
+| "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q"
 
 lemma single_less_eq_eval:
   "single x \<le> P \<longleftrightarrow> eval P x"
-  by (auto simp add: single_def less_eq_pred_def mem_def)
+  by (auto simp add: less_eq_pred_def le_fun_def)
 
 lemma contained_less_eq:
   "contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q"
@@ -934,9 +922,9 @@
   by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
 
 primrec null :: "'a seq \<Rightarrow> bool" where
-    "null Empty \<longleftrightarrow> True"
-  | "null (Insert x P) \<longleftrightarrow> False"
-  | "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
+  "null Empty \<longleftrightarrow> True"
+| "null (Insert x P) \<longleftrightarrow> False"
+| "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq"
 
 lemma null_is_empty:
   "null xq \<longleftrightarrow> is_empty (pred_of_seq xq)"
@@ -948,8 +936,8 @@
 
 primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where
   [code del]: "the_only dfault Empty = dfault ()"
-  | "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())"
-  | "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P
+| "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())"
+| "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P
        else let x = singleton dfault P; y = the_only dfault xq in
        if x = y then x else dfault ())"
 
@@ -973,23 +961,21 @@
    (auto simp add: Seq_def the_only_singleton is_empty_def
       null_is_empty singleton_bot singleton_single singleton_sup Let_def)
 
-definition not_unique :: "'a pred => 'a"
-where
-  [code del]: "not_unique A = (THE x. eval A x)"
-
-definition the :: "'a pred => 'a"
-where
+definition the :: "'a pred \<Rightarrow> 'a" where
   "the A = (THE x. eval A x)"
 
 lemma the_eqI:
   "(THE x. eval P x) = x \<Longrightarrow> the P = x"
   by (simp add: the_def)
 
+definition not_unique :: "'a pred \<Rightarrow> 'a" where
+  [code del]: "not_unique A = (THE x. eval A x)"
+
+code_abort not_unique
+
 lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A"
   by (rule the_eqI) (simp add: singleton_def not_unique_def)
 
-code_abort not_unique
-
 code_reflect Predicate
   datatypes pred = Seq and seq = Empty | Insert | Join
   functions map
diff -r 8382f4c2470c -r aae9c9a0735e src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Aug 22 18:15:33 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 23 07:12:05 2011 -0700
@@ -348,7 +348,6 @@
   Scan.optional ($$ "," |-- parse_annotation
                  --| Scan.option ($$ "," |-- parse_annotations)) []
 
-val vampire_unknown_fact = "unknown"
 val waldmeister_conjecture = "conjecture_1"
 
 val tofof_fact_prefix = "fof_"
@@ -408,9 +407,7 @@
               case deps of
                 ["file", _, s] =>
                 ((num,
-                  if s = vampire_unknown_fact then
-                    NONE
-                  else if s = waldmeister_conjecture then
+                  if s = waldmeister_conjecture then
                     find_formula_in_problem problem (mk_anot phi)
                   else
                     SOME [s |> perhaps (try (unprefix tofof_fact_prefix))]),
diff -r 8382f4c2470c -r aae9c9a0735e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 22 18:15:33 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 07:12:05 2011 -0700
@@ -21,9 +21,8 @@
      known_failures : (failure * string) list,
      conj_sym_kind : formula_kind,
      prem_kind : formula_kind,
-     formats : format list,
      best_slices :
-       Proof.context -> (real * (bool * (int * string * string))) list}
+       Proof.context -> (real * (bool * (int * format * string * string))) list}
 
   val force_sos : bool Config.T
   val e_smartN : string
@@ -46,12 +45,12 @@
   val snarkN : string
   val e_tofofN : string
   val waldmeisterN : string
-  val z3_atpN : string
+  val z3_tptpN : string
   val remote_prefix : string
   val remote_atp :
     string -> string -> string list -> (string * string) list
-    -> (failure * string) list -> formula_kind -> formula_kind -> format list
-    -> (Proof.context -> int * string) -> string * atp_config
+    -> (failure * string) list -> formula_kind -> formula_kind
+    -> (Proof.context -> int * format * string) -> string * atp_config
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val supported_atps : theory -> string list
@@ -78,9 +77,8 @@
    known_failures : (failure * string) list,
    conj_sym_kind : formula_kind,
    prem_kind : formula_kind,
-   formats : format list,
    best_slices :
-     Proof.context -> (real * (bool * (int * string * string))) list}
+     Proof.context -> (real * (bool * (int * format * string * string))) list}
 
 (* "best_slices" must be found empirically, taking a wholistic approach since
    the ATPs are run in parallel. The "real" components give the faction of the
@@ -106,7 +104,7 @@
 val satallaxN = "satallax"
 val spassN = "spass"
 val vampireN = "vampire"
-val z3_atpN = "z3_atp"
+val z3_tptpN = "z3_tptp"
 val e_sineN = "e_sine"
 val snarkN = "snark"
 val e_tofofN = "e_tofof"
@@ -132,6 +130,8 @@
 
 (* E *)
 
+fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
+
 val tstp_proof_delims =
   [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
    ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
@@ -190,8 +190,6 @@
     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
     \FIFOWeight(PreferProcessed))'"
 
-fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
-
 fun effective_e_weight_method ctxt =
   if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
 
@@ -214,16 +212,15 @@
       (OutOfResources, "SZS status ResourceOut")],
    conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
-   formats = [FOF],
    best_slices = fn ctxt =>
      let val method = effective_e_weight_method ctxt in
        (* FUDGE *)
        if method = e_smartN then
-         [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))),
-          (0.334, (true, (50, "mangled_guards?", e_fun_weightN))),
-          (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
+         [(0.333, (true, (500, FOF, "mangled_tags?", e_fun_weightN))),
+          (0.334, (true, (50, FOF, "mangled_guards?", e_fun_weightN))),
+          (0.333, (true, (1000, FOF, "mangled_tags?", e_sym_offset_weightN)))]
        else
-         [(1.0, (true, (500, "mangled_tags?", method)))]
+         [(1.0, (true, (500, FOF, "mangled_tags?", method)))]
      end}
 
 val e = (eN, e_config)
@@ -242,11 +239,10 @@
    known_failures = [],
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
-   formats = [THF Without_Choice, FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.667, (false, (150, "simple_higher", sosN))),
-      (0.333, (true, (50, "simple_higher", no_sosN)))]
+     [(0.667, (false, (150, THF Without_Choice, "simple_higher", sosN))),
+      (0.333, (true, (50, THF Without_Choice, "simple_higher", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -265,8 +261,8 @@
    known_failures = [(ProofMissing, "SZS status Theorem")],
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
-   formats = [THF With_Choice],
-   best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
+   best_slices =
+     K [(1.0, (true, (100, THF With_Choice, "simple_higher", "")))] (* FUDGE *)}
 
 val satallax = (satallaxN, satallax_config)
 
@@ -295,12 +291,11 @@
       (InternalError, "Please report this error")],
    conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
-   formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, "mangled_tags", sosN))),
-      (0.333, (false, (300, "poly_tags?", sosN))),
-      (0.334, (true, (50, "mangled_tags?", no_sosN)))]
+     [(0.333, (false, (150, FOF, "mangled_tags", sosN))),
+      (0.333, (false, (300, FOF, "poly_tags?", sosN))),
+      (0.334, (true, (50, FOF, "mangled_tags?", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -309,12 +304,16 @@
 
 (* Vampire *)
 
+fun is_old_vampire_version () =
+  string_ord (getenv "VAMPIRE_VERSION", "1.8") = LESS
+
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
    arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
-     "--proof tptp --mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
-     " --thanks \"Andrei and Krystof\" --input_file"
+     "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
+     " --proof tptp --output_axiom_names on \
+     \ --thanks \"Andrei and Krystof\" --input_file"
      |> sos = sosN ? prefix "--sos on ",
    proof_delims =
      [("=========== Refutation ==========",
@@ -333,12 +332,15 @@
       (Interrupted, "Aborted by signal SIGINT")],
    conj_sym_kind = Conjecture,
    prem_kind = Conjecture,
-   formats = [FOF],
    best_slices = fn ctxt =>
      (* FUDGE *)
-     [(0.333, (false, (150, "poly_guards", sosN))),
-      (0.334, (true, (50, "mangled_guards?", no_sosN))),
-      (0.333, (false, (500, "mangled_tags?", sosN)))]
+     (0.333, (false, (150, FOF, "poly_guards", sosN))) ::
+     (if is_old_vampire_version () then
+        [(0.334, (true, (50, FOF, "mangled_guards?", no_sosN))),
+         (0.333, (false, (500, FOF, "mangled_tags?", sosN)))]
+      else
+        [(0.334, (true, (50, TFF, "simple", no_sosN))),
+         (0.333, (false, (500, TFF, "simple", sosN)))])
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
@@ -347,29 +349,28 @@
 
 (* Z3 with TPTP syntax *)
 
-val z3_atp_config : atp_config =
+val z3_tptp_config : atp_config =
   {exec = ("Z3_HOME", "z3"),
    required_execs = [],
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
-     "MBQI=true -p -t:" ^ string_of_int (to_secs 1 timeout),
+     "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
    proof_delims = [],
    known_failures =
-     [(Unprovable, "\nsat"),
-      (GaveUp, "\nunknown"),
-      (GaveUp, "SZS status Satisfiable"),
-      (ProofMissing, "\nunsat"),
-      (ProofMissing, "SZS status Unsatisfiable")],
+     [(GaveUp, "SZS status Satisfiable"),
+      (GaveUp, "SZS status CounterSatisfiable"),
+      (GaveUp, "SZS status GaveUp"),
+      (ProofMissing, "SZS status Unsatisfiable"),
+      (ProofMissing, "SZS status Theorem")],
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
-   formats = [FOF],
    best_slices =
-     (* FUDGE (FIXME) *)
-     K [(0.5, (false, (250, "mangled_guards?", ""))),
-        (0.25, (false, (125, "mangled_guards?", ""))),
-        (0.125, (false, (62, "mangled_guards?", ""))),
-        (0.125, (false, (31, "mangled_guards?", "")))]}
+     (* FUDGE *)
+     K [(0.5, (false, (250, TFF, "simple", ""))),
+        (0.25, (false, (125, TFF, "simple", ""))),
+        (0.125, (false, (62, TFF, "simple", ""))),
+        (0.125, (false, (31, TFF, "simple", "")))]}
 
-val z3_atp = (z3_atpN, z3_atp_config)
+val z3_tptp = (z3_tptpN, z3_tptp_config)
 
 
 (* Remote ATP invocation via SystemOnTPTP *)
@@ -407,7 +408,7 @@
 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
 
 fun remote_config system_name system_versions proof_delims known_failures
-                  conj_sym_kind prem_kind formats best_slice : atp_config =
+                  conj_sym_kind prem_kind best_slice : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
@@ -425,58 +426,56 @@
       (Inappropriate, "says Inappropriate")],
    conj_sym_kind = conj_sym_kind,
    prem_kind = prem_kind,
-   formats = formats,
    best_slices = fn ctxt =>
-     let val (max_relevant, type_enc) = best_slice ctxt in
-       [(1.0, (false, (max_relevant, type_enc, "")))]
+     let val (max_relevant, format, type_enc) = best_slice ctxt in
+       [(1.0, (false, (max_relevant, format, type_enc, "")))]
      end}
 
 fun remotify_config system_name system_versions best_slice
-        ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats, ...}
+        ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
          : atp_config) : atp_config =
   remote_config system_name system_versions proof_delims known_failures
-                conj_sym_kind prem_kind formats best_slice
+                conj_sym_kind prem_kind best_slice
 
 fun remote_atp name system_name system_versions proof_delims known_failures
-        conj_sym_kind prem_kind formats best_slice =
+               conj_sym_kind prem_kind best_slice =
   (remote_prefix ^ name,
    remote_config system_name system_versions proof_delims known_failures
-                 conj_sym_kind prem_kind formats best_slice)
+                 conj_sym_kind prem_kind best_slice)
 fun remotify_atp (name, config) system_name system_versions best_slice =
   (remote_prefix ^ name,
    remotify_config system_name system_versions best_slice config)
 
 val remote_e =
   remotify_atp e "EP" ["1.0", "1.1", "1.2"]
-               (K (750, "mangled_tags?") (* FUDGE *))
+               (K (750, FOF, "mangled_tags?") (* FUDGE *))
 val remote_leo2 =
   remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
-               (K (100, "simple_higher") (* FUDGE *))
+               (K (100, THF Without_Choice, "simple_higher") (* FUDGE *))
 val remote_satallax =
   remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
-               (K (100, "simple_higher") (* FUDGE *))
+               (K (100, THF With_Choice, "simple_higher") (* FUDGE *))
 val remote_vampire =
-  remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
-               (K (200, "mangled_guards?") (* FUDGE *))
-val remote_z3_atp =
-  remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
+  remotify_atp vampire "Vampire" ["1.8"] (K (250, TFF, "simple") (* FUDGE *))
+val remote_z3_tptp =
+  remotify_atp z3_tptp "Z3" ["3.0"] (K (250, TFF, "simple") (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
-             Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
+             Conjecture (K (500, FOF, "mangled_guards?") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
-             [TFF, FOF] (K (100, "simple") (* FUDGE *))
+             (K (100, TFF, "simple") (* FUDGE *))
 val remote_e_tofof =
   remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
-             Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
+             Axiom Hypothesis (K (150, TFF, "simple") (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
              [("#START OF PROOF", "Proved Goals:")]
              [(OutOfResources, "Too many function symbols"),
               (Crashed, "Unrecoverable Segmentation Fault")]
-             Hypothesis Hypothesis [CNF_UEQ]
-             (K (50, "mangled_tags?") (* FUDGE *))
+             Hypothesis Hypothesis
+             (K (50, CNF_UEQ, "mangled_tags?") (* FUDGE *))
 
 (* Setup *)
 
@@ -499,8 +498,8 @@
   Synchronized.change systems (fn _ => get_systems ())
 
 val atps =
-  [e, leo2, satallax, spass, vampire, z3_atp, remote_e, remote_leo2,
-   remote_satallax, remote_vampire, remote_z3_atp, remote_e_sine, remote_snark,
+  [e, leo2, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
+   remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
    remote_e_tofof, remote_waldmeister]
 val setup = fold add_atp atps
 
diff -r 8382f4c2470c -r aae9c9a0735e src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 18:15:33 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 07:12:05 2011 -0700
@@ -90,7 +90,7 @@
   val level_of_type_enc : type_enc -> type_level
   val is_type_enc_quasi_sound : type_enc -> bool
   val is_type_enc_fairly_sound : type_enc -> bool
-  val choose_format : format list -> type_enc -> format * type_enc
+  val adjust_type_enc : format -> type_enc -> type_enc
   val mk_aconns :
     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
   val unmangled_const : string -> string * (string, 'b) ho_term list
@@ -611,23 +611,14 @@
   | is_type_level_monotonicity_based Fin_Nonmono_Types = true
   | is_type_level_monotonicity_based _ = false
 
-fun choose_format formats (Simple_Types (order, level)) =
-    (case find_first is_format_thf formats of
-       SOME format => (format, Simple_Types (order, level))
-     | NONE =>
-       if member (op =) formats TFF then
-         (TFF, Simple_Types (First_Order, level))
-       else
-         choose_format formats (Guards (Mangled_Monomorphic, level, Uniform)))
-  | choose_format formats type_enc =
-    (case hd formats of
-       CNF_UEQ =>
-       (CNF_UEQ, case type_enc of
-                   Guards stuff =>
-                   (if is_type_enc_fairly_sound type_enc then Tags else Guards)
-                       stuff
-                 | _ => type_enc)
-     | format => (format, type_enc))
+fun adjust_type_enc (THF _) type_enc = type_enc
+  | adjust_type_enc TFF (Simple_Types (_, level)) =
+    Simple_Types (First_Order, level)
+  | adjust_type_enc format (Simple_Types (_, level)) =
+    adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
+  | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
+    (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
+  | adjust_type_enc _ type_enc = type_enc
 
 fun lift_lambdas ctxt type_enc =
   map (close_form o Envir.eta_contract) #> rpair ctxt
@@ -2087,7 +2078,7 @@
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
         lambda_trans readable_names preproc hyp_ts concl_t facts =
   let
-    val (format, type_enc) = choose_format [format] type_enc
+    val type_enc = type_enc |> adjust_type_enc format
     val lambda_trans =
       if lambda_trans = smartN then
         if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
diff -r 8382f4c2470c -r aae9c9a0735e src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Aug 22 18:15:33 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 23 07:12:05 2011 -0700
@@ -154,7 +154,9 @@
 fun is_unit_equational_atp ctxt name =
   let val thy = Proof_Context.theory_of ctxt in
     case try (get_atp thy) name of
-      SOME {formats, ...} => member (op =) formats CNF_UEQ
+      SOME {best_slices, ...} =>
+      exists (fn (_, (_, (_, format, _, _))) => format = CNF_UEQ)
+             (best_slices ctxt)
     | NONE => false
   end
 
@@ -512,10 +514,10 @@
    them each time. *)
 val atp_important_message_keep_quotient = 10
 
-fun choose_format_and_type_enc soundness best_type_enc formats =
+fun choose_type_enc soundness best_type_enc format =
   the_default best_type_enc
   #> type_enc_from_string soundness
-  #> choose_format formats
+  #> adjust_type_enc format
 
 val metis_minimize_max_time = seconds 2.0
 
@@ -534,13 +536,13 @@
   #> Config.put Monomorph.max_new_instances max_new_instances
   #> Config.put Monomorph.keep_partial_instances false
 
-(* Give the ATPs some slack before interrupting them the hard way. "z3_atp" on
+(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
    Linux appears to be the only ATP that does not honor its time limit. *)
 val atp_timeout_slack = seconds 1.0
 
 fun run_atp mode name
         ({exec, required_execs, arguments, proof_delims, known_failures,
-          conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
+          conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
         ({debug, verbose, overlord, type_enc, sound, max_relevant,
           max_mono_iters, max_new_mono_instances, isar_proof,
           isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
@@ -609,7 +611,8 @@
                 |> maps (fn (name, rths) => map (pair name o snd) rths)
               end
             fun run_slice (slice, (time_frac, (complete,
-                                    (best_max_relevant, best_type_enc, extra))))
+                                    (best_max_relevant, format, best_type_enc,
+                                     extra))))
                           time_left =
               let
                 val num_facts =
@@ -623,9 +626,8 @@
                       Sound
                   else
                     Unsound
-                val (format, type_enc) =
-                  choose_format_and_type_enc soundness best_type_enc formats
-                                             type_enc
+                val type_enc =
+                  type_enc |> choose_type_enc soundness best_type_enc format
                 val fairly_sound = is_type_enc_fairly_sound type_enc
                 val facts =
                   facts |> map untranslated_fact