README.md

@@ -60,11 +60,11 @@ Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_
 ```
 $ pantograph Init
 goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
-goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"}
-goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"}
+goal.tactic {"stateId": 0, "tactic": "intro n m"}
+goal.tactic {"stateId": 1, "tactic": "assumption"}
 goal.delete {"stateIds": [0]}
 stat {}
-goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
+goal.tactic {"stateId": 1, "tactic": "rw [Nat.add_comm]"}
 stat
 ```
 where the application of `assumption` should lead to a failure.

doc/rationale.md

@@ -37,10 +37,6 @@ differently from Lean in some times, but never at the sacrifice of soundness.
 - When Lean LSP says "unresolved goals", that means a proof cannot finish where
   it is supposed to finish at the end of a `by` block. Pantograph will raise the
   error in this case, since it indicates the termination of a proof search branch.
-- `pick_goal` or `swap` will not work since they run contrary to tree search
-  paradigms. However, if there are tactics which perform non-trivial operations
-  to multiple goals at the same time, this constrain could potentially be
-  relaxed at a cost of great bookkeeping overhead to the user.
 
 Pantograph cannot perform things that are inherently constrained by Lean. These
 include: