src/Pure/General/graph.ML
changeset 13510 0a0f37f9c031
parent 12451 0224f472be71
child 14161 73ad4884441f
equal deleted inserted replaced
13509:6f168374652a 13510:0a0f37f9c031