ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
the keyword "inductive" making the theory file fail
ZF/Makefile: now has Inductive.thy,.ML
ZF/Datatype,Finite,Zorn: depend upon Inductive
ZF/intr_elim: now checks that the inductive name does not clash with
existing theory names
ZF/ind_section: deleted things replicated in Pure/section_utils.ML
ZF/ROOT: now loads Pure/section_utils
#! /bin/sh
# xlisten -- start a program in one window and create a listener window
# environment variable $LISTEN specifies the file name
#create the file!
date > $LISTEN
xterm -geo 80x10+0+0 -T Listener -n Listener -e tail -f $LISTEN &
sleep 2
xterm -geo 80x45+0-0 -e teeinput $* &