equal
deleted
inserted
replaced
1 (* Title: Pure/General/graph.ML |
1 (* Title: Pure/General/graph.ML |
2 ID: $Id$ |
|
3 Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
2 Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
4 |
3 |
5 Directed graphs. |
4 Directed graphs. |
6 *) |
5 *) |
7 |
6 |