equal
deleted
inserted
replaced
3 Copyright 1998 University of Cambridge |
3 Copyright 1998 University of Cambridge |
4 |
4 |
5 From Misra, "A Logic for Concurrent Programming", 1994 |
5 From Misra, "A Logic for Concurrent Programming", 1994 |
6 *) |
6 *) |
7 |
7 |
8 header{*Fixed Point of a Program*} |
8 section{*Fixed Point of a Program*} |
9 |
9 |
10 theory FP imports UNITY begin |
10 theory FP imports UNITY begin |
11 |
11 |
12 definition FP_Orig :: "'a program => 'a set" where |
12 definition FP_Orig :: "'a program => 'a set" where |
13 "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}" |
13 "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}" |