equal
deleted
inserted
replaced
34 (*Encoding using powerset of the desired axiom |
34 (*Encoding using powerset of the desired axiom |
35 (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F |
35 (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F |
36 *) |
36 *) |
37 Union "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F" |
37 Union "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F" |
38 |
38 |
39 monos "[Pow_mono]" |
39 monos Pow_mono |
40 |
40 |
41 |
41 |
42 |
42 |
43 constdefs (*visible version of the relation*) |
43 constdefs (*visible version of the relation*) |
44 leadsTo :: "['a set, 'a set] => 'a program set" |
44 leadsTo :: "['a set, 'a set] => 'a program set" |