equal
deleted
inserted
replaced
8 The state is identified with the one variable in existence. |
8 The state is identified with the one variable in existence. |
9 |
9 |
10 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1. |
10 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1. |
11 *) |
11 *) |
12 |
12 |
13 theory Common imports UNITY_Main begin |
13 theory Common imports "../UNITY_Main" begin |
14 |
14 |
15 consts |
15 consts |
16 ftime :: "nat=>nat" |
16 ftime :: "nat=>nat" |
17 gtime :: "nat=>nat" |
17 gtime :: "nat=>nat" |
18 |
18 |