Revising the Client proof as suggested by Michel Charpentier. New lemmas
about composition (in Union.ML), etc. Also changed "length" to "size"
because it is displayed as "size" in any event.
#!/bin/bash
#
# $Id$
#
# DESCRIPTION: Isabelle make utility
PRG=$(basename $0)
function usage()
{
echo
echo "Usage: $PRG [ARGS ...]"
echo
echo " Compiles logic in current directory using IsaMakefile."
echo " ARGS are directly passed to the system make program."
echo
exit 1
}
## main
[ "$1" = "-?" ] && usage
exec make -f IsaMakefile "$@"