merge

return right theorems

more (co)data docs

tuned proofs about 'convex'

more (co)data docs

tuned proofs;

treat all dummy type variables separately (in contrast to fca432074fb2);

removed dead code (see also 69d4543811d0);

merged

tuned signature;

more antiquotations -- avoid unchecked string literals;

more explicit exception pattern (NB: unqualified exceptions without arguments are in danger of becoming catch-all patterns by accident);

distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions; some notes about missing ML interface;

tuned white space; avoid "object-oriented English";

adhoc check of ML sources, in addition to thy files already covered in Thy_Load;

proper Isabelle symbols -- no UTF8 here;

proper Cygwin mirror for Isabelle2013-1;

explicit test of quick_and_dirty, which is rarely used in practice;

updated to cygwin-20130916;

more CHECKLIST;

updated cygwin snapshot;

updated to smlnj 110.76;

prefer high-level ML_System.share_common_data, ML_System.save_state -- except for bootstrap images (RAW, Pure);

more NEWS;

merge

prove simp theorems for newly generated definitions

example using restoring Transfer/Lifting context

use lifting_forget for deregistering numeric types as a quotient type

restoring Transfer/Lifting context

make ML function for deleting quotients public

public access to the raw transfer rules - for restoring transferring

another move to avoid sporadic kill of poly, which is presumably due to resource management on lxbroy2, lxbroy3 etc.;