'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;

updated comment;

more uniform signature;

uniform cert_vars/read_vars;

eliminated dead code;

clarified certify vs. sharing;

tuned;

NEWS;

added ML antiquotation @{attributes};

merged

made SML/NJ happy

simplified Locale.add_thmss, after partial evaluation of attributes;

misc tuning;

tuned;

refined partial evaluation of attributes: avoid duplication of facts for plain declarations; tuned;

discontinued slightly odd write_prv, which would still write .prv files the first time, and deprive add-on tools from date stamp change (cf. 157e74588c49);

do not store vacuous theorem specifications -- relevant for frugal local theory content; tuned;

put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory; tuned;

sequential lemmas to accomodate static rule attributes;

partial evaluation of locale facts leads to static scoping of rule attributes;

tuned message;

gave SML/NJ a chance

more robust options

adding another example for lifting definitions

improving header

more "metis" calls in example

be more silent when auto minimizing

less offensive terminology

more "metis" calls in example

minor textual improvement