src/Pure/defs.ML
changeset 20145 922b4e7b8efd
parent 19806 f860b7a98445
child 20390 c80247278cb6