src/Pure/defs.ML
changeset 20302 265b2342cf21
parent 19806 f860b7a98445
child 20390 c80247278cb6