src/HOL/ex/Term.ML
changeset 1633 9cb70937b426
parent 1476 608483c2122a
child 1811 9083542fd861