src/HOL/UNITY/SubstAx.thy
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5620 3ac11c4af76a
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
     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 prg A B ==
    15 		 leadsTo (Acts prg)
    16                          (reachable prg  Int  A)
    17   		         (reachable prg  Int  B)"
    18 end