src/Pure/tactic.ML
changeset 1072 0140ff702b23
parent 952 9e10962866b0
child 1077 c2df11ae8b55