author | paulson |
Wed, 08 Aug 2001 14:33:10 +0200 | |
changeset 11479 | 697dcaaf478f |
child 12195 | ed2893765a08 |
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:condition. ALL B:condition. F : stable(A Int B)})" FP :: i=>i "FP(F) == {s:state. F : stable({s})}" end