src/Pure/defs.ML
changeset 70842 c5caf81aa523
parent 70586 57df8a85317a
child 70920 1e0ad25c94c8