src/Pure/tactic.ML
changeset 15304 3514ca74ac54
parent 15021 6012f983a79f
child 15442 3b75e1b22ff1