src/HOL/UNITY/SubstAx.thy
author paulson
Wed Oct 07 10:32:00 1998 +0200 (1998-10-07)
changeset 5620 3ac11c4af76a
parent 5313 1861a564d7e2
child 5648 fe887910e32e
permissions -rw-r--r--
tidying and renaming
     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 LeadsTo relation: restricted to the set of reachable states.
     7 *)
     8 
     9 SubstAx = WFair + Constrains + 
    10 
    11 constdefs
    12 
    13    LeadsTo :: "['a program, 'a set, 'a set] => bool"
    14     "LeadsTo F A B ==
    15 		 leadsTo (Acts F)
    16                          (reachable F  Int  A)
    17   		         (reachable F  Int  B)"
    18 end