diff --git a/docs/devel/HowToTaclet.md b/docs/devel/HowToTaclet.md
index 50e06c3..6852bc6 100644
--- a/docs/devel/HowToTaclet.md
+++ b/docs/devel/HowToTaclet.md
@@ -76,8 +76,9 @@ The first branch is labeled "CUT: #cutFormula TRUE".
 In this branch, the found sub-term is replaced with true (`\replacewith(true)`), and the found sub-term is added as a new sequent formula to the antecedent: `\add(cutFormula ==>)`.
 
 A particular branch of the taclet can be tagged by enclosing the tag in brackets.
+This tag must be written after the branch label.
 The first branch in this example is tagged with "main".
-This tag must be written after the label.
+This particular value causes the branch to be visually continued on the parent branch if [the linearized Proof Tree mode](../../user/ProofTreeLinearMode/) is active.
 
 The second branch of the taclet is labeled "CUT: #cutFormula FALSE".
 In this branch, the found sub-term is replaced with false (`\replacewith(false)`), and the found sub-term is added as a new sequent formula to the succedent: `\add( ==> cutFormula)`.
diff --git a/docs/user/ProofTreeLinearMode.md b/docs/user/ProofTreeLinearMode.md
index 5d033e5..b70057a 100644
--- a/docs/user/ProofTreeLinearMode.md
+++ b/docs/user/ProofTreeLinearMode.md
@@ -1,4 +1,4 @@
-# Proof Tree: linearized symbolic execution
+# Proof Tree: linearized mode
 
 In the proof tree settings, you can enable the "Linearize Proof Tree" option.
 
diff --git a/docs/user/UiFeatures/index.md b/docs/user/UiFeatures/index.md
index 026e78d..d70a409 100644
--- a/docs/user/UiFeatures/index.md
+++ b/docs/user/UiFeatures/index.md
@@ -2,4 +2,4 @@
 - [Node Differences](../NodeDiff)
 - [Proof Slicing](../ProofSlicing)
 - [Proof Caching](../ProofCaching)
-- [Proof Tree: linearized symbolic execution](../ProofTreeLinearMode)
\ No newline at end of file
+- [Proof Tree: linearized mode](../ProofTreeLinearMode)
\ No newline at end of file