src/Pure/defs.ML
changeset 20452 6d8b29c7a960
parent 20390 c80247278cb6
child 20668 00521d5e1838