diff -r 6dfdb69e83ef -r b3bdc1abc7d3 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Nov 07 14:49:09 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Nov 07 15:07:02 2006 +0100
@@ -792,7 +792,7 @@
 code_const "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!(_ : IntInf.int = _)")
 
-subsubsection {* typedecls interpretated by customary serializations *}
+subsubsection {* typedecls interpreted by customary serializations *}
 
 text {*
   A common idiom is to use unspecified types for formalizations
@@ -966,9 +966,9 @@
 
 text {*
   This reveals the function equation @{thm insert_def}
-  for @{const insert}, which is operationally meaningsless
+  for @{const insert}, which is operationally meaningless
   but forces an equality constraint on the set members
-  (which is not fullfiable if the set members are functions).
+  (which is not satisfiable if the set members are functions).
   Even when using set of natural numbers (which are an instance
   of \emph{eq}), we run into a problem:
 *}
@@ -1156,7 +1156,7 @@
   \item @{ML_type CodegenConsts.const} is the identifier type:
      the product of a \emph{string} with a list of \emph{typs}.
      The \emph{string} is the constant name as represented inside Isabelle;
-     the \emph{typs} are a type instantion in the sense of System F,
+     the \emph{typs} are a type instantiation in the sense of System F,
      with canonical names for type variables.
 
   \item @{ML CodegenConsts.norm_of_typ}~@{text thy}~@{text "(constname, typ)"}
@@ -1230,7 +1230,7 @@
      @{text const} to executable content.
 
   \item @{ML CodegenData.add_inline}~@{text "thm"}~@{text "thy"} adds
-     inlineing theorem @{text thm} to executable content.
+     inlining theorem @{text thm} to executable content.
 
   \item @{ML CodegenData.del_inline}~@{text "thm"}~@{text "thy"} remove
      inlining theorem @{text thm} from executable content, if present.
@@ -1252,10 +1252,10 @@
      a datatype to executable content, with type constructor
      @{text name} and specification @{text spec}; @{text spec} is
      a pair consisting of a list of type variable with sort
-     contraints and a list of constructors with name
+     constraints and a list of constructors with name
      and types of arguments.  The addition as datatype
      has to be justified giving a certificate of suspended
-     theorems as wittnesses for injectiveness and distincness.
+     theorems as witnesses for injectiveness and distinctness.
 
   \item @{ML CodegenData.del_datatype}~@{text "name"}~@{text "thy"}
      remove a datatype from executable content, if present.
@@ -1296,7 +1296,7 @@
   \item @{ML CodegenFuncgr.make}~@{text thy}~@{text cs}
     returns a normalized function equation system,
     with the assertion that it contains any function
-    definition for constants @{text cs} (if exisiting).
+    definition for constants @{text cs} (if existing).
 
   \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text c}
     retrieves function definition for constant @{text c}.