| changeset 6575 | 70d758762c50 |
| parent 6536 | 281d44905cab |
| child 8041 | e3237d8c18d6 |
| 6574:a91b4cfd3104 | 6575:70d758762c50 |
|---|---|
11 consts |
11 consts |
12 LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) |
12 LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) |
13 |
13 |
14 defs |
14 defs |
15 LeadsTo_def |
15 LeadsTo_def |
16 "A LeadsTo B == {F. F : (reachable F Int A) leadsTo |
16 "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}" |
17 (reachable F Int B)}" |
|
18 end |
17 end |