src/HOL/UNITY/SubstAx.thy
author paulson
Thu Apr 29 10:51:58 1999 +0200 (1999-04-29)
changeset 6536 281d44905cab
parent 5648 fe887910e32e
child 6575 70d758762c50
permissions -rw-r--r--
made many specification operators infix
     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 consts
    12    LeadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
    13 
    14 defs
    15    LeadsTo_def
    16     "A LeadsTo B == {F. F : (reachable F  Int  A) leadsTo
    17 	   	            (reachable F  Int  B)}"
    18 end