Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed (now illegal) semicolons in generated theory files
authorblanchet
Mon, 22 Jun 2015 16:56:03 +0200
changeset 60544 3daf5eacec05
parent 60543 ea2778854739
child 60545 bcd11dcd0d90
removed (now illegal) semicolons in generated theory files
src/HOL/TPTP/lib/Tools/tptp_isabelle file | annotate | diff | comparison | revisions
src/HOL/TPTP/lib/Tools/tptp_isabelle_hot file | annotate | diff | comparison | revisions
src/HOL/TPTP/lib/Tools/tptp_nitpick file | annotate | diff | comparison | revisions
src/HOL/TPTP/lib/Tools/tptp_refute file | annotate | diff | comparison | revisions
src/HOL/TPTP/lib/Tools/tptp_sledgehammer file | annotate | diff | comparison | revisions
src/HOL/TPTP/lib/Tools/tptp_translate file | annotate | diff | comparison | revisions 
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
isabelle