src/Pure/context_position.ML
changeset 24630 351a308ab58d
parent 23354 a189707c1d76
child 24773 ec3a04e6f1a9
equal deleted inserted replaced
24629:65947eb930fa 24630:351a308ab58d