shrink: compress terms and types;
prefer member/insert over polymorphic mem/ins;
* 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.htmlDave MacQueen <dbm@research.bell-labs.com>