# HG changeset patch # User blanchet # Date 1434984963 -7200 # Node ID 3daf5eacec051a461f6a0be12e1f4a4625e30f72 # Parent ea2778854739256ee9857341854d1791dad22ce8 removed (now illegal) semicolons in generated theory files diff -r ea2778854739 -r 3daf5eacec05 src/HOL/TPTP/lib/Tools/tptp_isabelle --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Mon Jun 22 16:56:03 2015 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Mon Jun 22 16:56:03 2015 +0200 @@ -27,7 +27,7 @@ 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;" \ +ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" done diff -r ea2778854739 -r 3daf5eacec05 src/HOL/TPTP/lib/Tools/tptp_isabelle_hot --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Mon Jun 22 16:56:03 2015 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot Mon Jun 22 16:56:03 2015 +0200 @@ -27,7 +27,7 @@ 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;" \ +ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" done diff -r ea2778854739 -r 3daf5eacec05 src/HOL/TPTP/lib/Tools/tptp_nitpick --- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Mon Jun 22 16:56:03 2015 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Mon Jun 22 16:56:03 2015 +0200 @@ -27,7 +27,7 @@ for FILE in "$@" do echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ -ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ +ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" done diff -r ea2778854739 -r 3daf5eacec05 src/HOL/TPTP/lib/Tools/tptp_refute --- a/src/HOL/TPTP/lib/Tools/tptp_refute Mon Jun 22 16:56:03 2015 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_refute Mon Jun 22 16:56:03 2015 +0200 @@ -26,7 +26,7 @@ for FILE in "$@" do echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ -ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ +ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" done diff -r ea2778854739 -r 3daf5eacec05 src/HOL/TPTP/lib/Tools/tptp_sledgehammer --- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Mon Jun 22 16:56:03 2015 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Mon Jun 22 16:56:03 2015 +0200 @@ -27,7 +27,7 @@ for FILE in "$@" do echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ -ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \ +ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory" done diff -r ea2778854739 -r 3daf5eacec05 src/HOL/TPTP/lib/Tools/tptp_translate --- a/src/HOL/TPTP/lib/Tools/tptp_translate Mon Jun 22 16:56:03 2015 +0200 +++ b/src/HOL/TPTP/lib/Tools/tptp_translate Mon Jun 22 16:56:03 2015 +0200 @@ -24,6 +24,6 @@ args=("$@") echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ -ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end;" \ +ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \ > /tmp/$SCRATCH.thy "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory"