src/Pure/tactic.ML
changeset 12902 a23dc0b7566f
parent 12847 afa356dbcb15
child 13105 3d1e7a199bdc