author  paulson 
Thu, 02 Jul 1998 16:53:55 +0200  
changeset 5111  8f4b72f0c15d 
parent 4776  1f9362e769c1 
child 5253  82a5ca6290aa 
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 

6 
My treatment of the Substitution Axiom  not as an axiom! 

7 
*) 

8 

9 
SubstAx = WFair + 

10 

11 
constdefs 

12 

5111  13 
LeadsTo :: "['a set * ('a * 'a)set set, 'a set, 'a set] => bool" 
14 
"LeadsTo == %(Init,Acts) A B. 

15 
leadsTo Acts (reachable (Init,Acts) Int A) 

16 
(reachable (Init,Acts) Int B)" 

4776  17 

18 

19 
end 