1.1 --- a/doc-src/Codegen/Thy/Refinement.thy	Sat Nov 27 18:51:04 2010 +0100
     1.2 +++ b/doc-src/Codegen/Thy/Refinement.thy	Sat Nov 27 18:51:04 2010 +0100
     1.3 @@ -131,34 +131,40 @@
     1.4  
     1.5  lemma %quote empty_AQueue [code]:
     1.6    "empty = AQueue [] []"
     1.7 -  unfolding AQueue_def empty_def by simp
     1.8 +  by (simp add: AQueue_def empty_def)
     1.9  
    1.10  lemma %quote enqueue_AQueue [code]:
    1.11    "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
    1.12 -  unfolding AQueue_def by simp
    1.13 +  by (simp add: AQueue_def)
    1.14  
    1.15  lemma %quote dequeue_AQueue [code]:
    1.16    "dequeue (AQueue xs []) =
    1.17      (if xs = [] then (None, AQueue [] [])
    1.18      else dequeue (AQueue [] (rev xs)))"
    1.19    "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
    1.20 -  unfolding AQueue_def by simp_all
    1.21 +  by (simp_all add: AQueue_def)
    1.22  
    1.23  text {*
    1.24 -  \noindent For completeness, we provide a substitute for the
    1.25 -  @{text case} combinator on queues:
    1.26 +  \noindent It is good style, although no absolute requirement, to
    1.27 +  provide code equations for the original artefacts of the implemented
    1.28 +  type, if possible; in our case, these are the datatype constructor
    1.29 +  @{const Queue} and the case combinator @{const queue_case}:
    1.30  *}
    1.31  
    1.32 +lemma %quote Queue_AQueue [code]:
    1.33 +  "Queue = AQueue []"
    1.34 +  by (simp add: AQueue_def fun_eq_iff)
    1.35 +
    1.36  lemma %quote queue_case_AQueue [code]:
    1.37    "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
    1.38 -  unfolding AQueue_def by simp
    1.39 +  by (simp add: AQueue_def)
    1.40  
    1.41  text {*
    1.42    \noindent The resulting code looks as expected:
    1.43  *}
    1.44  
    1.45  text %quotetypewriter {*
    1.46 -  @{code_stmts empty enqueue dequeue (SML)}
    1.47 +  @{code_stmts empty enqueue dequeue Queue queue_case (SML)}
    1.48  *}
    1.49  
    1.50  text {*
    1.51 @@ -260,7 +266,7 @@
    1.52  text {*
    1.53    Typical data structures implemented by representations involving
    1.54    invariants are available in the library, e.g.~theories @{theory
    1.55 -  Fset} and @{theory Mapping} specify sets (type @{typ "'a fset"}) and
    1.56 +  Cset} and @{theory Mapping} specify sets (type @{typ "'a Cset.set"}) and
    1.57    key-value-mappings (type @{typ "('a, 'b) mapping"}) respectively;
    1.58    these can be implemented by distinct lists as presented here as
    1.59    example (theory @{theory Dlist}) and red-black-trees respectively