diff -r fe9cfe076c23 -r fa6c5d62adf5 doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Mon Jan 19 08:16:43 2009 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Mon Jan 19 13:37:24 2009 +0100
@@ -128,7 +128,7 @@
       \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}};
@@ -153,12 +153,12 @@
   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
@@ -168,7 +168,7 @@
 
     \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
@@ -177,7 +177,7 @@
       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
@@ -185,12 +185,12 @@
       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.
+      of code equations.
 
-    \item These defining equations are \qn{translated} to a program
+    \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