src/Pure/tctical.ML
changeset 3872 a5839ecee7b8
parent 3669 3384c6f1f095
child 3991 4cb2f2422695