| changeset 40361 | c409827db57d |
| parent 40359 | 84388bba911d |
| child 41229 | d797baa3d57c |
| 40360:1a73b5b90a3c | 40361:c409827db57d |
|---|---|
144 "_sdo_cons (_sdo_let p t) (_sdo_final s)" |
144 "_sdo_cons (_sdo_let p t) (_sdo_final s)" |
145 == "_sdo_final (let p = t in s)" |
145 == "_sdo_final (let p = t in s)" |
146 "_sdo_block (_sdo_final e)" => "e" |
146 "_sdo_block (_sdo_final e)" => "e" |
147 |
147 |
148 text {* |
148 text {* |
149 For an example, see @{text HOL/Proofs/Extraction/Higman.thy}. |
149 For an example, see @{text "HOL/Proofs/Extraction/Higman.thy"}. |
150 *} |
150 *} |
151 |
151 |
152 end |
152 end |