src/Pure/tactic.ML
changeset 13049 ce180e5b7fa0
parent 12847 afa356dbcb15
child 13105 3d1e7a199bdc