doc-src/Codegen/Thy/Program.thy
changeset 37427 e482f206821e
parent 37211 32a6f471f090
child 37612 48fed6598be9
equal deleted inserted replaced
37426:04d58897bf90 37427:e482f206821e
   132 
   132 
   133 text %quote {*@{code_stmts bexp (Haskell)}*}
   133 text %quote {*@{code_stmts bexp (Haskell)}*}
   134 
   134 
   135 text {*
   135 text {*
   136   \noindent This is a convenient place to show how explicit dictionary construction
   136   \noindent This is a convenient place to show how explicit dictionary construction
   137   manifests in generated code (here, the same example in @{text SML}):
   137   manifests in generated code (here, the same example in @{text SML})
       
   138   \cite{Haftmann-Nipkow:2010:code}:
   138 *}
   139 *}
   139 
   140 
   140 text %quote {*@{code_stmts bexp (SML)}*}
   141 text %quote {*@{code_stmts bexp (SML)}*}
   141 
   142 
   142 text {*
   143 text {*