src/Pure/tactic.ML
changeset 435 ca5356bd315a
parent 270 d506ea00c825
child 439 ad3f46c13f1e