src/HOL/UNITY/FP.thy
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5648 fe887910e32e
permissions -rw-r--r--
New UNITY theory
     1 (*  Title:      HOL/UNITY/FP
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Fixed Point of a Program
     7 
     8 From Misra, "A Logic for Concurrent Programming", 1994
     9 *)
    10 
    11 FP = UNITY +
    12 
    13 constdefs
    14 
    15   FP_Orig :: "('a * 'a)set set => 'a set"
    16     "FP_Orig Acts == Union{A. ALL B. stable Acts (A Int B)}"
    17 
    18   FP :: "('a * 'a)set set => 'a set"
    19     "FP Acts == {s. stable Acts {s}}"
    20 
    21 end