author | ehmety |
Thu, 15 Nov 2001 15:07:16 +0100 | |
changeset 12195 | ed2893765a08 |
parent 11479 | 697dcaaf478f |
child 14092 | 68da54626309 |
permissions | -rw-r--r-- |
(* Title: ZF/UNITY/FP.thy ID: $Id$ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge Fixed Point of a Program From Misra, "A Logic for Concurrent Programming", 1994 Theory ported from HOL. *) FP = UNITY + constdefs FP_Orig :: i=>i "FP_Orig(F) == Union({A:Pow(state). ALL B. F : stable(A Int B)})" FP :: i=>i "FP(F) == {s:state. F : stable({s})}" end