Document effect of tagging a branch 'main'

KeYProject · Jan 29, 2024 · f89bcad · f89bcad
1 parent 2f04ab4
commit f89bcad
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git 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
@@ -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
@@ -2,4 +2,4 @@
 - [Node Differences](../NodeDiff)
 - [Proof Slicing](../ProofSlicing)
 - [Proof Caching](../ProofCaching)
-- [Proof Tree: linearized symbolic execution](../ProofTreeLinearMode)
+- [Proof Tree: linearized mode](../ProofTreeLinearMode)