auto_quickcheck ref: set default in ProofGeneral/preferences only (retains responsiveness of plain tty interaction); auto_quickcheck: more messages, less complicated code;

ProofGeneral/preferences: auto_quickcheck=true;

qualified Proofterm.proofs;

@{const}: improved ProofContext.read_const does the job;

locale_const: suppress in class body as well (prevents qualified printing);

notation: improved ProofContext.read_const does the job;

updated;

replaced @{const} (allows name only) by proper @{term};

proper implementation of check phase; non-qualified names for class operations

explicit message for failed autoquickcheck

tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;

avoid obsolete Sign.read_prop;

tuned proofs -- avoid implicit prems;

fixed imports path;

tuned proofs -- avoid open cases;

function package: using the names of the equations as case names turned out to be impractical => disabled

avoid name clashes when generating code for union, inter

oops -- avoid vacous goal message; tuned messages;

tuned messages; tuned;

avoid "import" as identifier, which is a keyword in Alice;

tuned presentation;

avoid implicit use of prems; tuned proofs;

where/of: do not allow schematic variables here!

removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy; discontinued legacy_intern_skolem, gen_read';

discontinued legacy vars;

removed unused read_def_terms';

eliminated illegal schematic variables in where/of;

eliminated illegal schematic variables in where/of; tuned;

x86_64: fall back on x86 (more efficient);

tuned comments;

renamed ProofContext.read_const' to ProofContext.read_const_proper;

renamed ProofContext.read_const' to ProofContext.read_const_proper; export expand_abbrevs;