src/HOL/UNITY/SubstAx.thy
author paulson
Thu Jan 13 17:30:23 2000 +0100 (2000-01-13)
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.
     1 (*  Title:      HOL/UNITY/SubstAx
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Weak LeadsTo relation (restricted to the set of reachable states)
     7 *)
     8 
     9 SubstAx = WFair + Constrains + 
    10 
    11 constdefs
    12    Ensures :: "['a set, 'a set] => 'a program set"            (infixl 60)
    13     "A Ensures B == {F. F : (reachable F Int A) ensures B}"
    14 
    15    LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
    16     "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
    17 
    18 end