doc-src/IsarImplementation/Thy/prelim.thy

   \item @{ML_functor TheoryDataFun}@{text "(spec)"} declares data for
   type @{ML_type theory} according to the specification provided as
   argument structure.  The resulting structure provides data init and
   access operations as described above.
 
-  \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous for
-  type @{ML_type Proof.context}.
-
-  \item @{ML_functor GenericDataFun}@{text "(spec)"} is analogous for
-  type @{ML_type Context.generic}.
+  \item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous to
+  @{ML_functor TheoryDataFun} for type @{ML_type Proof.context}.
+
+  \item @{ML_functor GenericDataFun}@{text "(spec)"} is analogous to
+  @{ML_functor TheoryDataFun} for type @{ML_type Context.generic}.
 
   \end{description}
 *}
 
 
 section {* Name spaces *}
 
 text {*
+  FIXME tune
+
   By general convention, each kind of formal entities (logical
   constant, type, type class, theorem, method etc.) lives in a
   separate name space.  It is usually clear from the syntactic context
   of a name, which kind of entity it refers to.  For example, proof
   method @{text "foo"} vs.\ theorem @{text "foo"} vs.\ logical

 
 
 subsection {* Strings of symbols *}
 
 text {*
+  FIXME tune
+
   Isabelle strings consist of a sequence of
   symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
   subsumes plain ASCII characters as well as an infinite collection of
   named symbols (for greek, math etc.).}, which are either packed as
   an actual @{text "string"}, or represented as a list.  Each symbol

 
 
 subsection {* Qualified names *}
 
 text {*
+  FIXME tune
+
   A \emph{qualified name} essentially consists of a non-empty list of
   basic name components.  The packad notation uses a dot as separator,
   as in @{text "A.b"}, for example.  The very last component is called
   \emph{base} name, the remaining prefix \emph{qualifier} (which may
   be empty).