src/Doc/Codegen/Refinement.thy

 text %quotetypewriter {*
   @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
 *}
 
 text {*
+  See further \cite{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement}
+  for the meta theory of datatype refinement involving invariants.
+
   Typical data structures implemented by representations involving
   invariants are available in the library, theory @{theory Mapping}
   specifies key-value-mappings (type @{typ "('a, 'b) mapping"});
   these can be implemented by red-black-trees (theory @{theory RBT}).
 *}