| author | paulson |
| Thu, 13 Jan 2000 17:30:23 +0100 | |
| changeset 8122 | b43ad07660b9 |
| parent 8041 | e3237d8c18d6 |
| child 9685 | 6d123a7e30bd |
| permissions | -rw-r--r-- |
| paulson@4776 | 1 |
(* Title: HOL/UNITY/SubstAx |
| paulson@4776 | 2 |
ID: $Id$ |
| paulson@4776 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
| paulson@4776 | 4 |
Copyright 1998 University of Cambridge |
| paulson@4776 | 5 |
|
| paulson@6536 | 6 |
Weak LeadsTo relation (restricted to the set of reachable states) |
| paulson@4776 | 7 |
*) |
| paulson@4776 | 8 |
|
| paulson@5313 | 9 |
SubstAx = WFair + Constrains + |
| paulson@4776 | 10 |
|
| paulson@8041 | 11 |
constdefs |
| paulson@8122 | 12 |
Ensures :: "['a set, 'a set] => 'a program set" (infixl 60) |
| paulson@8122 | 13 |
"A Ensures B == {F. F : (reachable F Int A) ensures B}"
|
| paulson@8122 | 14 |
|
| paulson@8041 | 15 |
LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) |
| paulson@8041 | 16 |
"A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
|
| paulson@4776 | 17 |
|
| paulson@4776 | 18 |
end |