src/Pure/tactic.ML
changeset 18394 fa0674cd6df1
parent 18209 6bcd9b2ca49b
child 18471 ca9a864018d6