author  paulson 
Thu, 15 Oct 1998 11:35:07 +0200  
changeset 5648  fe887910e32e 
parent 5620  3ac11c4af76a 
child 6536  281d44905cab 
permissions  rwrr 
4776  1 
(* Title: HOL/UNITY/SubstAx 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

5277
e4297d03e5d2
A higherlevel treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5253
diff
changeset

6 
LeadsTo relation: restricted to the set of reachable states. 
4776  7 
*) 
8 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

9 
SubstAx = WFair + Constrains + 
4776  10 

11 
constdefs 

12 

5648  13 
LeadsTo :: "['a set, 'a set] => 'a program set" 
14 
"LeadsTo A B == {F. F : leadsTo (reachable F Int A) 

15 
(reachable F Int B)}" 

4776  16 
end 