equal
deleted
inserted
replaced
20 |
20 |
21 SCRATCH="Scratch_${PRG}_$$_${RANDOM}" |
21 SCRATCH="Scratch_${PRG}_$$_${RANDOM}" |
22 |
22 |
23 for FILE in "$@" |
23 for FILE in "$@" |
24 do |
24 do |
25 echo "theory $SCRATCH imports \"Main\" begin ML {* ATP_Problem_Generate.translate_tptp_file \"$FILE\" *} end;" \ |
25 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
|
26 ML {* ATP_Problem_Import.translate_tptp_file \"$FILE\" *} end;" \ |
26 > /tmp/$SCRATCH.thy |
27 > /tmp/$SCRATCH.thy |
27 "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" |
28 "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" |
28 done |
29 done |