--- a/src/Doc/Implementation/Prelim.thy Fri Aug 28 23:48:03 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy Fri Aug 28 23:55:17 2015 +0200
@@ -80,13 +80,9 @@
ancestor theories. To this end, the system maintains a set of
symbolic ``identification stamps'' within each theory.
- The @{text "merge"} operation produces the least upper bound of two
- theories, which actually degenerates into absorption of one theory
- into the other (according to the nominal sub-theory relation).
-
- The @{text "begin"} operation starts a new theory by importing
- several parent theories and entering a special mode of nameless
- incremental updates, until the final @{text "end"} operation is
+ The @{text "begin"} operation starts a new theory by importing several
+ parent theories (with merged contents) and entering a special mode of
+ nameless incremental updates, until the final @{text "end"} operation is
performed.
\medskip The example in \figref{fig:ex-theory} below shows a theory
@@ -123,7 +119,6 @@
@{index_ML_type theory} \\
@{index_ML Context.eq_thy: "theory * theory -> bool"} \\
@{index_ML Context.subthy: "theory * theory -> bool"} \\
- @{index_ML Theory.merge: "theory * theory -> theory"} \\
@{index_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\
@{index_ML Theory.parents_of: "theory -> theory list"} \\
@{index_ML Theory.ancestors_of: "theory -> theory list"} \\
@@ -142,10 +137,6 @@
(@{text "\<subseteq>"}) of the corresponding content (according to the
semantics of the ML modules that implement the data).
- \item @{ML "Theory.merge"}~@{text "(thy\<^sub>1, thy\<^sub>2)"} absorbs one theory
- into the other. This version of ad-hoc theory merge fails for
- unrelated theories!
-
\item @{ML "Theory.begin_theory"}~@{text "name parents"} constructs
a new theory based on the given parents. This ML function is
normally not invoked directly.