author | paulson |
Wed, 18 Nov 1998 15:10:46 +0100 | |
changeset 5931 | 325300576da7 |
parent 5648 | fe887910e32e |
child 6536 | 281d44905cab |
permissions | -rw-r--r-- |
(* Title: HOL/UNITY/SubstAx ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge LeadsTo relation: restricted to the set of reachable states. *) SubstAx = WFair + Constrains + constdefs LeadsTo :: "['a set, 'a set] => 'a program set" "LeadsTo A B == {F. F : leadsTo (reachable F Int A) (reachable F Int B)}" end