# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID a4148c95134d99d6f48bb0eac793892bacf79646
# Parent  d7a6ad5d27bf3793bfd5dd80966eadfae8c0e86f
renamed TPTP commands to agree with Sutcliffe's terminology

diff -r d7a6ad5d27bf -r a4148c95134d src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Jun 06 10:35:05 2012 +0200
@@ -21,8 +21,8 @@
   val freeze_problem_consts : theory -> term -> term
   val make_conj : term list * term list -> term list -> term
   val sledgehammer_tptp_file : theory -> int -> string -> unit
-  val isabelle_demo_tptp_file : theory -> int -> string -> unit
-  val isabelle_comp_tptp_file : theory -> int -> string -> unit
+  val isabelle_tptp_file : theory -> int -> string -> unit
+  val isabelle_hot_tptp_file : theory -> int -> string -> unit
   val translate_tptp_file : string -> string -> string -> unit
 end;
 
@@ -285,7 +285,7 @@
     |> print_szs_from_success conjs
   end
 
-fun isabelle_tptp_file demo thy timeout file_name =
+fun generic_isabelle_tptp_file demo thy timeout file_name =
   let
     val (conjs, assms, ctxt) =
       read_tptp_file thy (freeze_problem_consts thy) file_name
@@ -300,8 +300,8 @@
     |> print_szs_from_success conjs
   end
 
-val isabelle_demo_tptp_file = isabelle_tptp_file true
-val isabelle_comp_tptp_file = isabelle_tptp_file false
+val isabelle_tptp_file = generic_isabelle_tptp_file false
+val isabelle_hot_tptp_file = generic_isabelle_tptp_file true
 
 
 (** Translator between TPTP(-like) file formats **)
diff -r d7a6ad5d27bf -r a4148c95134d src/HOL/TPTP/lib/Tools/tptp_isabelle
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle	Wed Jun 06 10:35:05 2012 +0200
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# Author: Jasmin Blanchette
+#
+# DESCRIPTION: Isabelle tactics for TPTP competitive division
+
+
+PRG="$(basename "$0")"
+
+function usage() {
+  echo
+  echo "Usage: isabelle $PRG TIMEOUT FILES"
+  echo
+  echo "  Runs a combination of Isabelle tactics on TPTP problems."
+  echo "  Each problem is allocated at most TIMEOUT seconds."
+  echo
+  exit 1
+}
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+
+TIMEOUT=$1
+shift
+
+for FILE in "$@"
+do
+  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+    > /tmp/$SCRATCH.thy
+  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
+done
diff -r d7a6ad5d27bf -r a4148c95134d src/HOL/TPTP/lib/Tools/tptp_isabelle_comp
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_comp	Wed Jun 06 10:35:05 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Jasmin Blanchette
-#
-# DESCRIPTION: Isabelle tactics for TPTP competitive division
-
-
-PRG="$(basename "$0")"
-
-function usage() {
-  echo
-  echo "Usage: isabelle $PRG TIMEOUT FILES"
-  echo
-  echo "  Runs a combination of Isabelle tactics on TPTP problems."
-  echo "  Each problem is allocated at most TIMEOUT seconds."
-  echo
-  exit 1
-}
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
-
-TIMEOUT=$1
-shift
-
-for FILE in "$@"
-do
-  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.isabelle_comp_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
-    > /tmp/$SCRATCH.thy
-  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
-done
diff -r d7a6ad5d27bf -r a4148c95134d src/HOL/TPTP/lib/Tools/tptp_isabelle_demo
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_demo	Wed Jun 06 10:35:05 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Jasmin Blanchette
-#
-# DESCRIPTION: Isabelle tactics for TPTP demo division
-
-
-PRG="$(basename "$0")"
-
-function usage() {
-  echo
-  echo "Usage: isabelle $PRG TIMEOUT FILES"
-  echo
-  echo "  Runs a combination of Isabelle tactics on TPTP problems."
-  echo "  Each problem is allocated at most TIMEOUT seconds."
-  echo
-  exit 1
-}
-
-[ "$#" -eq 0 -o "$1" = "-?" ] && usage
-
-SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
-
-TIMEOUT=$1
-shift
-
-for FILE in "$@"
-do
-  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.isabelle_demo_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
-    > /tmp/$SCRATCH.thy
-  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
-done
diff -r d7a6ad5d27bf -r a4148c95134d src/HOL/TPTP/lib/Tools/tptp_isabelle_hot
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Wed Jun 06 10:35:05 2012 +0200
@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+#
+# Author: Jasmin Blanchette
+#
+# DESCRIPTION: Isabelle tactics for TPTP demo division
+
+
+PRG="$(basename "$0")"
+
+function usage() {
+  echo
+  echo "Usage: isabelle $PRG TIMEOUT FILES"
+  echo
+  echo "  Runs a combination of Isabelle tactics on TPTP problems."
+  echo "  Each problem is allocated at most TIMEOUT seconds."
+  echo
+  exit 1
+}
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+
+TIMEOUT=$1
+shift
+
+for FILE in "$@"
+do
+  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
+    > /tmp/$SCRATCH.thy
+  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
+done