src/Pure/tactic.ML
changeset 3942 1f1c1f524d19
parent 3706 e57b5902822f
child 3984 8fc76a487616