drop redundant fundef_cong rule

tuned

repair malformed fundef_cong rule

removed duplicate

tuned message: same error may occur in different contexts;

detect more errors;

merged

made sorted fun again

imported patch sorted

add lemma on lists from Falling_Factorial_Sum entry

merged

avoid evaluation of embedded comment;

disable "display" style in marginal (line) comment;

more uniform output of source / text / theory_text, with handling of formal comments etc.;

sort completion result;

recovered antiquotation check without latex mode (cf. dfc93f2b01ea);

formal treatment of documentation names;

support for completion;

adapted to a5ca98950a91;

tuned output of plain name;

clarified signature;

tuned;

tuned;

unused;

clarified access to antiquotation options; define explicit variants of antiquotations; output proper Latex.text; misc tuning and clarification;

more operations;

tuned signature;

discontinued unused wrapper: print_mode is provided directly;

corrected name

moved from AFP/Gromov