dropped warnings by dropping ineffective code declarations

standardized algebraic conventions: prefer a, b, c over x, y, z

uniform _ div _ as infix syntax for ring division

fixed several "inside-out" proofs

add transfer theorems for fixed points

Merge

tidied more proofs

misc tuning;

misc tuning;

unused;

misc tuning;

isabelle update_cartouches;

more user aliases;

merged

prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms;

tuned proofs;

clarified local after_qed: result is not exported yet; proper goal_export for show: 'if' is like 'assume';

support for "if prems" in local goal statements;

tuned message;

tuned proofs;

no need for protected goal (see 240ad53041c9);

tuned proofs;

prevent export of future result -- avoid interference with goal fixes;

more uniform treatment of auto bindings vs. explicit user bindings; misc tuning;

tuned signature;

allow for_fixes for 'have', 'show' etc.; tuned signature;

eliminated dead code;

clarified abstracted term bindings (again, see c8384ff11711);

tuned signature;

tuned;