src/Pure/tactic.ML
changeset 7487 c0f9b956a3e7
parent 7248 322151fe6f02
child 7491 95a4af0e10a7