src/Pure/tactic.ML
changeset 7186 860479291bb5
parent 6979 4b9963810121
child 7248 322151fe6f02