src/Pure/context.ML
changeset 28321 9f4499bf9384
parent 28317 83c4fc383409
child 28375 c879d88d038a
equal deleted inserted replaced
28320:c6aef67f964d 28321:9f4499bf9384