made tactics more robust
method language markup, e.g. relevant to prevent outer keyword completion;
suppress completion of obscure keyword, avoid confusion with plain "simp";
tuned signature;
tuned;
prefer proof context over background theory
obsolete workaround
markup for method combinators;
improved rendering of blinking cursor;
more precise before_caret_range (looking both in space and time);
replaced smt-based proof with metis proof that requires no external tool
transfer domain rule for special case of functions - was missing
tuned specifications and proofs;
merged
intermediate typedef for the type of the bound (local to lfp)