repeat
repeat
は、指定したタクティクを失敗するまで繰り返します。
variable (P Q R S T : Prop)
example : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by
repeat intro
repeat apply_assumption
repeat
は、指定したタクティクを失敗するまで繰り返します。
variable (P Q R S T : Prop)
example : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by
repeat intro
repeat apply_assumption