src/HOL/ex/Term.ML
changeset 1556 2fd82cec17d4
parent 1476 608483c2122a
child 1811 9083542fd861