src/Pure/context.ML
changeset 38987 96fae8916d8b
parent 37871 c7ce7685e087
child 39020 ac0f24f850c9
equal deleted inserted replaced
38986:e34c1b09bb5e 38987:96fae8916d8b