src/Pure/tactic.ML
changeset 2197 e895937fcd56
parent 2145 5e8db0bc195e
child 2228 f381c1a98209