src/Pure/defs.ML
changeset 20183 fd546b0c8a7c
parent 19806 f860b7a98445
child 20390 c80247278cb6