src/Pure/tactic.ML
changeset 558 c4092ae47210
parent 439 ad3f46c13f1e
child 670 ff4c6691de9d