src/Pure/context.ML
changeset 38820 d0f98bd81a85
parent 37871 c7ce7685e087
child 39020 ac0f24f850c9
equal deleted inserted replaced
38819:71c9f61516cd 38820:d0f98bd81a85