author paulson
Thu, 13 Jan 2000 17:30:23 +0100
changeset 8122 b43ad07660b9
parent 8041 e3237d8c18d6
child 9685 6d123a7e30bd
permissions -rw-r--r--
working version, with Alloc now working on the same state space as the whole system. Partial removal of ELT.

(*  Title:      HOL/UNITY/SubstAx
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Weak LeadsTo relation (restricted to the set of reachable states)

SubstAx = WFair + Constrains + 

   Ensures :: "['a set, 'a set] => 'a program set"            (infixl 60)
    "A Ensures B == {F. F : (reachable F Int A) ensures B}"

   LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"