tuned output

tuned names

merged;

more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed; transfer theorems where they are picked from the theory; tuned;

no fork from draft thy -- avoid potential for crash via classrel_proof/arity_proof;

merged

export some generally useful operations;

tuned comment -- do not claim anything;

cleaner context threading

tuned output

slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);

put single-theorem names before multi-theorem ones (broken since 5d147d492792)

get rid of spurious "Isar" proofs

also generate queries for goals with too many Isar dependencies

updated to scala-2.10.0;

merged

tuned message

tap after, not before command invocation

increased hard timeout -- minimization can take time

nicer output

pass option to minimize

prefer apple.laf.useScreenMenuBar=true (despite cf. effcfa38e77b) to make it work better with full-screen mode;

ignore vacuous edits (e.g. stemming from Plugin.init_models) to avoid pointless protocol round-trip, which could lead to painting of outdated snapshot in the meantime (notably on Windows);

tuned JEDIT_JAVA_OPTIONS: increase chances that it works with approx. 8 cores and 32bit platform (notably Windows);