src/Pure/General/graph.ML
changeset 48573 de82a584bc2a
parent 48350 09bf3b73e446
child 49560 11430dd89e35