Focus

特定のサブゴールだけを表示するようにするコマンド。

2 subgoals
  
  b : bool
  ============================
   true = true /\ true = false

subgoal 2 is:
 false = true /\ false = false

Unnamed_thm < Focus 1.
1 subgoal
  
  b : bool
  ============================
   true = true /\ true = false

サブゴールの番号を省略すると、Focus 1となる。

元に戻すときは、Unfocus.