# HG changeset patch
# User wenzelm
# Date 1265107669 -3600
# Node ID c4cd364119832dbdc66a239095e7ee8946063e6f
# Parent  c4c02ac736a6684d634b402e8d482352166e15cd
moved examples to proper place;

diff -r c4c02ac736a6 -r c4cd36411983 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Feb 01 22:46:12 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Tue Feb 02 11:47:49 2010 +0100
@@ -209,85 +209,6 @@
   \end{description}
 *}
 
-text %mlex {*
-  The following artificial example demonstrates theory
-  data: we maintain a set of terms that are supposed to be wellformed
-  wrt.\ the enclosing theory.  The public interface is as follows:
-*}
-
-ML {*
-signature WELLFORMED_TERMS =
-sig
-  val get: theory -> term list
-  val add: term -> theory -> theory
-end;
-*}
-
-text {* \noindent The implementation uses private theory data
-  internally, and only exposes an operation that involves explicit
-  argument checking wrt.\ the given theory. *}
-
-ML {*
-structure Wellformed_Terms: WELLFORMED_TERMS =
-struct
-
-structure Terms = Theory_Data
-(
-  type T = term OrdList.T;
-  val empty = [];
-  val extend = I;
-  fun merge (ts1, ts2) =
-    OrdList.union TermOrd.fast_term_ord ts1 ts2;
-)
-
-val get = Terms.get;
-
-fun add raw_t thy =
-  let val t = Sign.cert_term thy raw_t
-  in Terms.map (OrdList.insert TermOrd.fast_term_ord t) thy end;
-
-end;
-*}
-
-text {* We use @{ML_type "term OrdList.T"} for reasonably efficient
-  representation of a set of terms: all operations are linear in the
-  number of stored elements.  Here we assume that our users do not
-  care about the declaration order, since that data structure forces
-  its own arrangement of elements.
-
-  Observe how the @{verbatim merge} operation joins the data slots of
-  the two constituents: @{ML OrdList.union} prevents duplication of
-  common data from different branches, thus avoiding the danger of
-  exponential blowup.  (Plain list append etc.\ must never be used for
-  theory data merges.)
-
-  \medskip Our intended invariant is achieved as follows:
-  \begin{enumerate}
-
-  \item @{ML Wellformed_Terms.add} only admits terms that have passed
-  the @{ML Sign.cert_term} check of the given theory at that point.
-
-  \item Wellformedness in the sense of @{ML Sign.cert_term} is
-  monotonic wrt.\ the sub-theory relation.  So our data can move
-  upwards in the hierarchy (via extension or merges), and maintain
-  wellformedness without further checks.
-
-  \end{enumerate}
-
-  Note that all basic operations of the inference kernel (which
-  includes @{ML Sign.cert_term}) observe this monotonicity principle,
-  but other user-space tools don't.  For example, fully-featured
-  type-inference via @{ML Syntax.check_term} (cf.\
-  \secref{sec:term-check}) is not necessarily monotonic wrt.\ the
-  background theory, since constraints of term constants can be
-  strengthened by later declarations, for example.
-
-  In most cases, user-space context data does not have to take such
-  invariants too seriously.  The situation is different in the
-  implementation of the inference kernel itself, which uses the very
-  same data mechanisms for types, constants, axioms etc.
-*}
-
 
 subsection {* Proof context \label{sec:context-proof} *}
 
@@ -487,6 +408,85 @@
   \end{description}
 *}
 
+text %mlex {*
+  The following artificial example demonstrates theory
+  data: we maintain a set of terms that are supposed to be wellformed
+  wrt.\ the enclosing theory.  The public interface is as follows:
+*}
+
+ML {*
+  signature WELLFORMED_TERMS =
+  sig
+    val get: theory -> term list
+    val add: term -> theory -> theory
+  end;
+*}
+
+text {* \noindent The implementation uses private theory data
+  internally, and only exposes an operation that involves explicit
+  argument checking wrt.\ the given theory. *}
+
+ML {*
+  structure Wellformed_Terms: WELLFORMED_TERMS =
+  struct
+
+  structure Terms = Theory_Data
+  (
+    type T = term OrdList.T;
+    val empty = [];
+    val extend = I;
+    fun merge (ts1, ts2) =
+      OrdList.union TermOrd.fast_term_ord ts1 ts2;
+  )
+
+  val get = Terms.get;
+
+  fun add raw_t thy =
+    let val t = Sign.cert_term thy raw_t
+    in Terms.map (OrdList.insert TermOrd.fast_term_ord t) thy end;
+
+  end;
+*}
+
+text {* We use @{ML_type "term OrdList.T"} for reasonably efficient
+  representation of a set of terms: all operations are linear in the
+  number of stored elements.  Here we assume that our users do not
+  care about the declaration order, since that data structure forces
+  its own arrangement of elements.
+
+  Observe how the @{verbatim merge} operation joins the data slots of
+  the two constituents: @{ML OrdList.union} prevents duplication of
+  common data from different branches, thus avoiding the danger of
+  exponential blowup.  (Plain list append etc.\ must never be used for
+  theory data merges.)
+
+  \medskip Our intended invariant is achieved as follows:
+  \begin{enumerate}
+
+  \item @{ML Wellformed_Terms.add} only admits terms that have passed
+  the @{ML Sign.cert_term} check of the given theory at that point.
+
+  \item Wellformedness in the sense of @{ML Sign.cert_term} is
+  monotonic wrt.\ the sub-theory relation.  So our data can move
+  upwards in the hierarchy (via extension or merges), and maintain
+  wellformedness without further checks.
+
+  \end{enumerate}
+
+  Note that all basic operations of the inference kernel (which
+  includes @{ML Sign.cert_term}) observe this monotonicity principle,
+  but other user-space tools don't.  For example, fully-featured
+  type-inference via @{ML Syntax.check_term} (cf.\
+  \secref{sec:term-check}) is not necessarily monotonic wrt.\ the
+  background theory, since constraints of term constants can be
+  strengthened by later declarations, for example.
+
+  In most cases, user-space context data does not have to take such
+  invariants too seriously.  The situation is different in the
+  implementation of the inference kernel itself, which uses the very
+  same data mechanisms for types, constants, axioms etc.
+*}
+
 
 section {* Names \label{sec:names} *}