src/Pure/tactic.ML
changeset 15992 cb02d70a2040
parent 15977 aa6744dd998e
child 16325 a6431098a929