| changeset 42463 | f270e3e18be5 |
| parent 37936 | 1e4c5015a72e |
| child 45605 | a89b4bc311a5 |
| 42462:0fd80c27fdf5 | 42463:f270e3e18be5 |
|---|---|
8 and 11.3. |
8 and 11.3. |
9 *) |
9 *) |
10 |
10 |
11 theory Reachability imports "../Detects" Reach begin |
11 theory Reachability imports "../Detects" Reach begin |
12 |
12 |
13 types edge = "(vertex*vertex)" |
13 type_synonym edge = "vertex * vertex" |
14 |
14 |
15 record state = |
15 record state = |
16 reach :: "vertex => bool" |
16 reach :: "vertex => bool" |
17 nmsg :: "edge => nat" |
17 nmsg :: "edge => nat" |
18 |
18 |