author | paulson |
Thu, 26 Aug 1999 11:33:24 +0200 | |
changeset 7359 | 98a2afab3f86 |
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