diff --git a/tests/lean/interactive/focus.lean.expected.out b/tests/lean/interactive/focus.lean.expected.out
index fafa3fc0ef..7b474dcd02 100644
--- a/tests/lean/interactive/focus.lean.expected.out
+++ b/tests/lean/interactive/focus.lean.expected.out
@@ -1,5 +1,5 @@
 {"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":4,"severity":"error","text":"focus tactic failed, insufficient number of tactics\nstate:\na b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ b = a"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"source":,"state":"a b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ a = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":5}
-{"record":{"source":,"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":7}
+{"record":{"doc":"`focus { t }` temporarily hides all goals other than the first, applies `t`, and then restores the other goals. It fails if there are no goals.","source":,"state":"a b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ a = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":5}
+{"record":{"doc":"`focus { t }` temporarily hides all goals other than the first, applies `t`, and then restores the other goals. It fails if there are no goals.","source":,"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":7}
 {"response":"ok","seq_num":9}
diff --git a/tests/lean/interactive/goal_info_rw.lean.expected.out b/tests/lean/interactive/goal_info_rw.lean.expected.out
index bee7228b45..b900c1c0a0 100644
--- a/tests/lean/interactive/goal_info_rw.lean.expected.out
+++ b/tests/lean/interactive/goal_info_rw.lean.expected.out
@@ -1,6 +1,6 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":3}
-{"record":{"source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":5}
+{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":3}
+{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = r","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":5}
 {"record":{"full-id":"h₁","state":"p q r : Prop,\nh₁ : p = q,\nh₂ : q = r\n⊢ q = q","type":"p = q"},"response":"ok","seq_num":7}
-{"record":{"source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":8}
-{"record":{"source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":10}
+{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":8}
+{"record":{"doc":"An abbreviation for `rewrite`.","source":,"state":"no goals","tactic_param_idx":0,"tactic_params":["([ (←? expr), ... ] | ←? expr)","(at (* | (⊢ | id)*))?","tactic.rewrite_cfg?"],"text":"rw","type":"interactive.parse tactic.interactive.rw_rules → interactive.parse interactive.types.location → opt_param tactic.rewrite_cfg {to_apply_cfg := {md := reducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt}, symm := ff, occs := occurrences.all} → tactic unit"},"response":"ok","seq_num":10}
diff --git a/tests/lean/interactive/info_goal.lean.expected.out b/tests/lean/interactive/info_goal.lean.expected.out
index 79d00b1b07..38ca49db28 100644
--- a/tests/lean/interactive/info_goal.lean.expected.out
+++ b/tests/lean/interactive/info_goal.lean.expected.out
@@ -1,5 +1,5 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"doc":"This tactic applies to any goal. It gives directly the exact proof\nterm of the goal. Let `T` be our goal, let `p` be a term of type `U` then\n`exact p` succeeds iff `T` and `U` are definitionally equal.","source":,"state":"⊢ ℕ → ℕ","tactic_params":["expr"],"text":"exact","type":"interactive.parse interactive.types.texpr → tactic unit"},"response":"ok","seq_num":4}
+{"record":{"doc":"This tactic provides an exact proof term to solve the main goal. If `t` is the goal and `p` is a term of type `u` then `exact p` succeeds if and only if `t` and ``u`` can be unified.","source":,"state":"⊢ ℕ → ℕ","tactic_params":["expr"],"text":"exact","type":"interactive.parse interactive.types.texpr → tactic unit"},"response":"ok","seq_num":4}
 {"record":{"state":"no goals"},"response":"ok","seq_num":6}
 {"record":{"state":"no goals"},"response":"ok","seq_num":8}
-{"record":{"doc":"This tactic applies to any goal. It gives directly the exact proof\nterm of the goal. Let `T` be our goal, let `p` be a term of type `U` then\n`exact p` succeeds iff `T` and `U` are definitionally equal.","source":,"state":"⊢ ℕ → ℕ","tactic_param_idx":0,"tactic_params":["expr"],"text":"exact","type":"interactive.parse interactive.types.texpr → tactic unit"},"response":"ok","seq_num":11}
+{"record":{"doc":"This tactic provides an exact proof term to solve the main goal. If `t` is the goal and `p` is a term of type `u` then `exact p` succeeds if and only if `t` and ``u`` can be unified.","source":,"state":"⊢ ℕ → ℕ","tactic_param_idx":0,"tactic_params":["expr"],"text":"exact","type":"interactive.parse interactive.types.texpr → tactic unit"},"response":"ok","seq_num":11}