- 'induct' method now derives symbolic cases from the *rulified* rule
(before it used to rulify cases stemming from the internal atomized
version); this means that the context of a non-atomic statement
becomes is included in the hypothesis, avoiding the slightly
cumbersome show "PROP ?case" form;
* Cambridge (UK)
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
* Munich (Germany)
http://isabelle.in.tum.de/dist/
* New Jersey (USA)
http://ftp.research.bell-labs.com/dist/smlnj/isabelle/source.html
Dave MacQueen <dbm@research.bell-labs.com>
* Stanford (USA)
ftp://rodin.stanford.edu/pub/smlnj/isabelle/source.html
Lal George (?)