src/Pure/tctical.ML
changeset 4962 e9217cb15b42
parent 4602 0e034d76932e
child 5141 495a4f9af897