wenzelm [Thu, 11 Dec 2008 12:02:48 +0100] rev 29060
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
more antiquotations;
explicit Theory.requires;
adapted to recent changes in ~~/src/HOL/Tools/typedef_package.ML;
misc tuning and simplification;