Isabelle/Isar（その13）

　また，1と名付けた事実の参照は，usingを用いて

  show "a 0 = 2 ^ 0 - 1"
    using 1 by simp

更にstaementの前に，fromを用いて

  from 1 show "a 0 = 2 ^ 0 - 1"
    by simp

とすることもできます．仮定に限らず一般の定理の参照も同様ですが，from，usingでは変数のタイプのマッチングを行わないので，参照はその証明内の事実に留めた方が無難です．

　なお，この例では仮定に1，2と明示的に名前を打ちましたが，システム内部で既に仮定全体にはassmsという名前が与えられていますので，例えば

  from assms(1) show "a 0 = 2 ^ 0 - 1"
    by simp

とすれば，命名は不要です．