src/Pure/General/source.ML
changeset 17740 fc385ce6187d
parent 15531 08c8dad8e399
child 19485 5385c9d86c2a
equal deleted inserted replaced
17739:eddebb044a62 17740:fc385ce6187d