src/Pure/General/graph.ML
changeset 46117 edd50ec8d471
parent 44338 700008399ee5
child 46611 669601fa1a62
equal deleted inserted replaced
46116:b903d272c37d 46117:edd50ec8d471