doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy

     \begin{tikzpicture}[x = 4.2cm, y = 1cm]
       \tikzstyle entity=[rounded corners, draw, thick, color = black, fill = white];
       \tikzstyle process=[ellipse, draw, thick, color = green, fill = white];
       \tikzstyle process_arrow=[->, semithick, color = green];
       \node (HOL) at (0, 4) [style=entity] {@{text "Isabelle/HOL"} theory};
-      \node (eqn) at (2, 2) [style=entity] {defining equations};
+      \node (eqn) at (2, 2) [style=entity] {code equations};
       \node (iml) at (2, 0) [style=entity] {intermediate language};
       \node (seri) at (1, 0) [style=process] {serialisation};
       \node (SML) at (0, 3) [style=entity] {@{text SML}};
       \node (OCaml) at (0, 2) [style=entity] {@{text OCaml}};
       \node (further) at (0, 1) [style=entity] {@{text "\<dots>"}};

   \end{figure}
 
   The code generator employs a notion of executability
   for three foundational executable ingredients known
   from functional programming:
-  \emph{defining equations}, \emph{datatypes}, and
-  \emph{type classes}.  A defining equation as a first approximation
+  \emph{code equations}, \emph{datatypes}, and
+  \emph{type classes}.  A code equation as a first approximation
   is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"}
   (an equation headed by a constant @{text f} with arguments
   @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}).
-  Code generation aims to turn defining equations
+  Code generation aims to turn code equations
   into a functional program.  This is achieved by three major
   components which operate sequentially, i.e. the result of one is
   the input
   of the next in the chain,  see diagram \ref{fig:arch}:
 
   \begin{itemize}
 
     \item Out of the vast collection of theorems proven in a
       \qn{theory}, a reasonable subset modelling
-      defining equations is \qn{selected}.
+      code equations is \qn{selected}.
 
     \item On those selected theorems, certain
       transformations are carried out
       (\qn{preprocessing}).  Their purpose is to turn theorems
       representing non- or badly executable
       specifications into equivalent but executable counterparts.
       The result is a structured collection of \qn{code theorems}.
 
-    \item Before the selected defining equations are continued with,
+    \item Before the selected code equations are continued with,
       they can be \qn{preprocessed}, i.e. subjected to theorem
       transformations.  This \qn{preprocessor} is an interface which
       allows to apply
       the full expressiveness of ML-based theorem transformations
       to code generation;  motivating examples are shown below, see
       \secref{sec:preproc}.
       The result of the preprocessing step is a structured collection
-      of defining equations.
-
-    \item These defining equations are \qn{translated} to a program
+      of code equations.
+
+    \item These code equations are \qn{translated} to a program
       in an abstract intermediate language.  Think of it as a kind
       of \qt{Mini-Haskell} with four \qn{statements}: @{text data}
-      (for datatypes), @{text fun} (stemming from defining equations),
+      (for datatypes), @{text fun} (stemming from code equations),
       also @{text class} and @{text inst} (for type classes).
 
     \item Finally, the abstract program is \qn{serialised} into concrete
       source code of a target language.