author | paulson |
Thu, 26 Aug 1999 11:33:24 +0200 | |
changeset 7359 | 98a2afab3f86 |
parent 6575 | 70d758762c50 |
child 8041 | e3237d8c18d6 |
permissions | -rw-r--r-- |
(* 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 B}" end