| changeset 29297 | 62e0f892e525 |
| parent 28421 | 05d202350b8d |
| child 29798 | 6df726203e39 |
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML Thu Jan 01 21:28:38 2009 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML Thu Jan 01 21:30:13 2009 +0100 @@ -11,7 +11,7 @@ datatype 'a queue = Queue of 'a list * 'a list; -val empty : 'a queue = Queue ([], []); +val empty : 'a queue = Queue ([], []) fun dequeue (Queue ([], [])) = (NONE, Queue ([], [])) | dequeue (Queue (xs, y :: ys)) = (SOME y, Queue (xs, ys))