added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers

--- a/src/HOL/IsaMakefile	Tue Mar 22 18:27:47 2011 +0100
+++ b/src/HOL/IsaMakefile	Tue Mar 22 18:38:29 2011 +0100
@@ -466,8 +466,8 @@
   Library/Sublist_Order.thy Library/Sum_of_Squares.thy			\
   Library/Sum_of_Squares/sos_wrapper.ML					\
   Library/Sum_of_Squares/sum_of_squares.ML				\
-  Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
-  Library/While_Combinator.thy Library/Zorn.thy				\
+  Library/TPTP.thy Library/Transitive_Closure_Table.thy			\
+  Library/Univ_Poly.thy Library/While_Combinator.thy Library/Zorn.thy	\
   $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
   Library/reflection.ML Library/reify_data.ML				\
   Library/Quickcheck_Narrowing.thy \

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/TPTP.thy	Tue Mar 22 18:38:29 2011 +0100
@@ -0,0 +1,50 @@
+theory TPTP
+imports Main
+uses "~~/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML"
+begin
+
+declare mem_def [simp add]
+
+declare [[smt_oracle]]
+
+ML {* proofs := 0 *}
+
+ML {*
+fun SOLVE_TIMEOUT seconds name tac st =
+  let
+    val result =
+      TimeLimit.timeLimit (Time.fromSeconds seconds)
+        (fn () => SINGLE (SOLVE tac) st) ()
+      handle TimeLimit.TimeOut => NONE
+        | ERROR _ => NONE
+  in
+    (case result of
+      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
+    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
+  end
+*}
+
+ML {*
+fun isabellep_tac max_secs =
+   SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
+       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
+       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
+   ORELSE
+   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
+   ORELSE
+   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
+*}
+
+end