equal
deleted
inserted
replaced
129 |
129 |
130 translations |
130 translations |
131 "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))" |
131 "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))" |
132 == "CONST scomp t (\<lambda>p. e)" |
132 == "CONST scomp t (\<lambda>p. e)" |
133 "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))" |
133 "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))" |
134 == "CONST fcomp t e" |
134 => "CONST fcomp t e" |
|
135 "_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))" |
|
136 <= "_sdo_final (CONST fcomp t e)" |
|
137 "_sdo_block (_sdo_cons (_sdo_then t) e)" |
|
138 <= "CONST fcomp t (_sdo_block e)" |
135 "_sdo_block (_sdo_cons (_sdo_let p t) bs)" |
139 "_sdo_block (_sdo_cons (_sdo_let p t) bs)" |
136 == "let p = t in _sdo_block bs" |
140 == "let p = t in _sdo_block bs" |
137 "_sdo_block (_sdo_cons b (_sdo_cons c cs))" |
141 "_sdo_block (_sdo_cons b (_sdo_cons c cs))" |
138 == "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))" |
142 == "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))" |
139 "_sdo_cons (_sdo_let p t) (_sdo_final s)" |
143 "_sdo_cons (_sdo_let p t) (_sdo_final s)" |