on 4e69658 help sign in
2 lines 105 B history raw
1ClaimAndUnfocus.idr:8:27-32:
2This style of tactic proof is deprecated. See %runElab for the replacement.