src/Pure/defs.ML
changeset 19997 fe69952f09f6
parent 19806 f860b7a98445
child 20390 c80247278cb6