equal
deleted
inserted
replaced
116 LOADER="tptp_graph_$RANDOM" |
116 LOADER="tptp_graph_$RANDOM" |
117 echo "theory $LOADER imports \"$TPTP_HOME/TPTP_Parser\" \ |
117 echo "theory $LOADER imports \"$TPTP_HOME/TPTP_Parser\" \ |
118 begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \ |
118 begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \ |
119 ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \ |
119 ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \ |
120 > $WORKDIR/$LOADER.thy |
120 > $WORKDIR/$LOADER.thy |
121 "$ISABELLE_TOOL" process -e "use_thy \"$WORKDIR/$LOADER\";" Pure |
121 isabelle process -e "use_thy \"$WORKDIR/$LOADER\";" Pure |
122 } |
122 } |
123 |
123 |
124 function cleanup_workdir() |
124 function cleanup_workdir() |
125 { |
125 { |
126 if [ -n "$KEEP_TEMP" ]; then |
126 if [ -n "$KEEP_TEMP" ]; then |