src/Pure/tactic.ML
changeset 11545 0b56d9c90dcf
parent 10817 083d4a6734b4
child 11671 994dc2efff55