equal
deleted
inserted
replaced
6 From Misra, "A Logic for Concurrent Programming", 1994 |
6 From Misra, "A Logic for Concurrent Programming", 1994 |
7 *) |
7 *) |
8 |
8 |
9 header{*Fixed Point of a Program*} |
9 header{*Fixed Point of a Program*} |
10 |
10 |
11 theory FP = UNITY: |
11 theory FP imports UNITY begin |
12 |
12 |
13 constdefs |
13 constdefs |
14 |
14 |
15 FP_Orig :: "'a program => 'a set" |
15 FP_Orig :: "'a program => 'a set" |
16 "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}" |
16 "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}" |