| changeset 11703 | 6e5de8d4290a |
| parent 9517 | f58863b1406a |
| child 12338 | de0f4a63baa5 |
| 11702:ebfe5ba905b0 | 11703:6e5de8d4290a |
|---|---|
81 PLegalReturner_def "PLegalReturner ch p == TEMP |
81 PLegalReturner_def "PLegalReturner ch p == TEMP |
82 [][ ? v. Return ch p v ]_((rtrner ch)!p)" |
82 [][ ? v. Return ch p v ]_((rtrner ch)!p)" |
83 LegalReturner_def "LegalReturner ch == TEMP (! p. PLegalReturner ch p)" |
83 LegalReturner_def "LegalReturner ch == TEMP (! p. PLegalReturner ch p)" |
84 |
84 |
85 end |
85 end |
86 |
|
87 |