src/Pure/tactic.ML
changeset 13828 fb6ec40dd291
parent 13650 31bd2a8cdbe2
child 13925 761af5c2fd59