src/Pure/tctical.ML
changeset 973 f57fb576520f
parent 922 196ca0973a6d
child 1458 fd510875fb71