src/Pure/tactic.ML
changeset 8831 b824c0c55613
parent 8129 29e239c7b8c2
child 8977 dd8bc754a072