src/Pure/tctical.ML
changeset 8594 d2e2a3df6871
parent 8535 7428194b39f7
child 10767 8fa4aafa7314