src/Pure/tactic.ML
changeset 11117 55358999077d
parent 10817 083d4a6734b4
child 11671 994dc2efff55