src/Pure/tactic.ML
changeset 11307 891fbd3f4881
parent 10817 083d4a6734b4
child 11671 994dc2efff55