| changeset 23854 | 688a8a7bcd4e |
| parent 23755 | 1c4672d130b1 |
| child 24345 | 86a3557a9ebb |
| 23853:2c69bb1374b8 | 23854:688a8a7bcd4e |
|---|---|
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 ExecutableSet |
9 imports Main SCT_Misc Kleene_Algebras Executable_Set |
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 = |