src/Pure/tactic.ML
changeset 31726 ffd2dc631d88
parent 31251 6ff48aa6142c
child 31794 71af1fd6a5e4