implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules

merged

more markup;

proper term equality; proper Args.term_pattern parser (like 'is' or 'let' in Isar);

tuned message;

more uniform treatment of dockables and their standard actions;

standardized action and panel names;

tuned imports;

prefer concrete list append;

tuned whitespace;