author | paulson |
Fri, 12 May 2000 15:05:02 +0200 | |
changeset 8862 | 78643f8449c6 |
parent 8122 | b43ad07660b9 |
child 9685 | 6d123a7e30bd |
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 + constdefs Ensures :: "['a set, 'a set] => 'a program set" (infixl 60) "A Ensures B == {F. F : (reachable F Int A) ensures B}" LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}" end