src/Pure/General/graph.ML
changeset 44502 c537d5e5a365
parent 44338 700008399ee5
child 46611 669601fa1a62