src/Pure/defs.ML
changeset 58726 cee57ab1f76f
parent 57520 3ad1b289f21b
child 59050 376446e98951
equal deleted inserted replaced
58725:9402a7f15ed5 58726:cee57ab1f76f