tuned

no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code

enable parallel proofs (cf. e8552cba702d), only affects packages so far; disable quick_and_dirty to make packages produce proofs -- NB: 'sorry' works via "int" mode of proof commands;

added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);

tuned proofs;

more robust update_perspective, e.g. required after reload of buffer that is not at start position;

tuned imports;

updated header keywords;

init message not bad;

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;

discontinued obsolete last_execs (cf. cd3ab7625519);

remove now-unnecessary type annotations from lift_definition commands

more robust generation of quotient rules using tactics

merged

add function dest_Quotient

standardized alias;

fixed document;

merged

correct plumbing of proof contexts, so that force_rty_type won't generalize more type variables than it should

detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr

make Quotient_Def.lift_raw_const working again

use standard quotient lemmas to generate transfer rules

add transfer lemmas for quotients

define reflp directly, in the manner of symp and transp

set up and use lift_definition for word operations

lift_definition declares transfer_rule attribute

configure transfer method for 'a word -> int

added timestamps to logging of named thms

merged

merged