author | berghofe |
Wed, 21 Oct 1998 17:57:02 +0200 | |
changeset 5721 | 458a67fd5461 |
parent 5648 | fe887910e32e |
child 13796 | 19f50fa807ae |
permissions | -rw-r--r-- |
(* Title: HOL/UNITY/FP ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Fixed Point of a Program From Misra, "A Logic for Concurrent Programming", 1994 *) FP = UNITY + constdefs FP_Orig :: "'a program => 'a set" "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}" FP :: "'a program => 'a set" "FP F == {s. F : stable {s}}" end