doc-src/IsarAdvanced/Codegen/Thy/Program.thy
changeset 28456 7a558c872104
parent 28447 df77ed974a78
child 28462 6ec603695aaf
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Thu Oct 02 12:17:20 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Thu Oct 02 13:07:33 2008 +0200
     1.3 @@ -27,7 +27,8 @@
     1.4  
     1.5  lemma %quoteme [code func]:
     1.6    "dequeue (Queue xs []) =
     1.7 -     (if xs = [] then (None, Queue [] []) else dequeue (Queue [] (rev xs)))"
     1.8 +     (if xs = [] then (None, Queue [] [])
     1.9 +       else dequeue (Queue [] (rev xs)))"
    1.10    "dequeue (Queue xs (y # ys)) =
    1.11       (Some y, Queue xs ys)"
    1.12    by (cases xs, simp_all) (cases "rev xs", simp_all)
    1.13 @@ -39,7 +40,7 @@
    1.14    the corresponding constant is determined syntactically.  The resulting code:
    1.15  *}
    1.16  
    1.17 -text %quoteme {*@{code_stmts empty enqueue dequeue (Haskell)}*}
    1.18 +text %quoteme {*@{code_stmts dequeue (consts) dequeue (Haskell)}*}
    1.19  
    1.20  text {*
    1.21    \noindent You may note that the equality test @{term "xs = []"} has been