| changeset 60770 | 240563fbf41d |
| parent 58871 | c399ae4b836f |
| child 76213 | e44d86131648 |
| 60769:cf7f3465eaf1 | 60770:240563fbf41d |
|---|---|
5 From Misra, "A Logic for Concurrent Programming", 1994 |
5 From Misra, "A Logic for Concurrent Programming", 1994 |
6 |
6 |
7 Theory ported from HOL. |
7 Theory ported from HOL. |
8 *) |
8 *) |
9 |
9 |
10 section{*Fixed Point of a Program*} |
10 section\<open>Fixed Point of a Program\<close> |
11 |
11 |
12 theory FP imports UNITY begin |
12 theory FP imports UNITY begin |
13 |
13 |
14 definition |
14 definition |
15 FP_Orig :: "i=>i" where |
15 FP_Orig :: "i=>i" where |