src/Pure/context.ML
changeset 11970 e7eedbd2c8ca
parent 11819 9283b3c11234
child 14976 65f572245276
equal deleted inserted replaced
11969:c850db2e2e98 11970:e7eedbd2c8ca