src/Pure/tctical.ML
changeset 13076 70704dd48bd5
parent 12851 e87496286934
child 13108 5fd62bcdff62