src/HOL/ex/Term.ML
changeset 1797 334308d2afbc
parent 1476 608483c2122a
child 1811 9083542fd861