* isatool mkdir provides easy setup of Isabelle session directories,
including proper documents;
* generated LaTeX sources are now deleted after successful run
(isatool document -c); may retain a copy somewhere else via -D option
of isatool usedir;
* old-style theories now produce (crude) LaTeX sources as well;
* compression of ML heaps images may now be controlled via -c option
of isabelle and isatool usedir;
Goal
"evala env (substa s a) = evala (%x. evala env (s x)) a & \
\ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
by(induct_tac "a b" 1);