doc-src/Codegen/Thy/Evaluation.thy
 changeset 40751 6975c4d83ffd parent 40350 1ef7ee8dd165 child 41184 5c6f44d22f51
equal inserted replaced
40740:6bff052e4f48 40751:6975c4d83ffd
     1 theory Evaluation
     1 theory Evaluation
     2 imports Setup
     2 imports Setup
     3 begin
     3 begin
     4
     4
     5 section {* Evaluation *}
     5 section {* Evaluation \label{sec:evaluation} *}
     6
     6
     7 text {*
     7 text {*
     8   Recalling \secref{sec:principle}, code generation turns a system of
     8   Recalling \secref{sec:principle}, code generation turns a system of
     9   equations into a program with the \emph{same} equational semantics.
     9   equations into a program with the \emph{same} equational semantics.
    10   As a consequence, this program can be used as a \emph{rewrite
    10   As a consequence, this program can be used as a \emph{rewrite