src/Pure/tactical.ML
changeset 80266 d52be75ae60b
parent 76051 854e9223767f