ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
called expandshort
#! /bin/sh
# teeinput -- start a program and log all inputs to a file
# environment variable $LISTEN specifies the file name
tee -a -i $LISTEN | $*