equal
deleted
inserted
replaced
7 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 |
7 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 |
8 *) |
8 *) |
9 |
9 |
10 theory Channel imports "../UNITY_Main" begin |
10 theory Channel imports "../UNITY_Main" begin |
11 |
11 |
12 types state = "nat set" |
12 type_synonym state = "nat set" |
13 |
13 |
14 consts |
14 consts |
15 F :: "state program" |
15 F :: "state program" |
16 |
16 |
17 definition minSet :: "nat set => nat option" where |
17 definition minSet :: "nat set => nat option" where |