src/HOL/UNITY/SubstAx.thy
author paulson
Thu, 29 Apr 1999 10:51:58 +0200
changeset 6536 281d44905cab
parent 5648 fe887910e32e
child 6575 70d758762c50
permissions -rw-r--r--
made many specification operators infix

(*  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 + 

consts
   LeadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)

defs
   LeadsTo_def
    "A LeadsTo B == {F. F : (reachable F  Int  A) leadsTo
	   	            (reachable F  Int  B)}"
end