src/Pure/General/graph.ML
changeset 35709 267e15230a31
parent 35405 fc130c5e81ec
child 35974 3a588b344749
equal deleted inserted replaced
35707:44936737902d 35709:267e15230a31