src/Pure/tactic.ML
changeset 18260 5597cfcecd49
parent 18209 6bcd9b2ca49b
child 18471 ca9a864018d6