src/Pure/tactic.ML
changeset 12866 c00df7765656
parent 12847 afa356dbcb15
child 13105 3d1e7a199bdc
equal deleted inserted replaced
12865:6b3484b8d572 12866:c00df7765656