| changeset 24423 | ae9cd0e92423 |
| parent 24345 | 86a3557a9ebb |
| 24422:c0b5ff9e9e4d | 24423:ae9cd0e92423 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* General Graphs as Sets *} |
6 header {* General Graphs as Sets *} |
7 |
7 |
8 theory Graphs |
8 theory Graphs |
9 imports Main SCT_Misc Kleene_Algebras Executable_Set |
9 imports Main SCT_Misc Kleene_Algebras |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Basic types, Size Change Graphs *} |
12 subsection {* Basic types, Size Change Graphs *} |
13 |
13 |
14 datatype ('a, 'b) graph = |
14 datatype ('a, 'b) graph = |