src/Pure/defs.ML
changeset 20083 717b1eb434f1
parent 19806 f860b7a98445
child 20390 c80247278cb6