eliminated THENL -- use THEN RANGE; eliminated TRY' -- use TRY with op o; observe naming convention ctxt: Proof.context; tuned whitespace;