src/Pure/tactic.ML
changeset 16740 a5ae2757dd09
parent 16666 9a987b59ecab
child 16809 8ca51a846576