diff -r eacb7825025d -r eb47307ab930 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Sun Oct 10 20:42:10 2010 +0100
+++ b/doc-src/Ref/theories.tex	Sun Oct 10 20:49:25 2010 +0100
@@ -7,37 +7,6 @@
 
 Isabelle's theory loader manages dependencies of the internal graph of theory
 nodes (the \emph{theory database}) and the external view of the file system.
-See \S\ref{sec:intro-theories} for its most basic commands, such as
-\texttt{use_thy}.  There are a few more operations available.
-
-\begin{ttbox}
-use_thy_only    : string -> unit
-update_thy_only : string -> unit
-touch_thy       : string -> unit
-remove_thy      : string -> unit
-delete_tmpfiles : bool ref \hfill\textbf{initially true}
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{use_thy_only} "$name$";] is similar to \texttt{use_thy},
-  but processes the actual theory file $name$\texttt{.thy} only, ignoring
-  $name$\texttt{.ML}.  This might be useful in replaying proof scripts by hand
-  from the very beginning, starting with the fresh theory.
-  
-\item[\ttindexbold{update_thy_only} "$name$";] is similar to
-  \texttt{update_thy}, but processes the actual theory file
-  $name$\texttt{.thy} only, ignoring $name$\texttt{.ML}.
-
-\item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the
-  internal graph as outdated.  While the theory remains usable, subsequent
-  operations such as \texttt{use_thy} may cause a reload.
-  
-\item[\ttindexbold{remove_thy} "$name$";] deletes theory node $name$,
-  including \emph{all} of its descendants.  Beware!  This is a quick way to
-  dispose a large number of theories at once.  Note that {\ML} bindings to
-  theorems etc.\ of removed theories may still persist.
-  
-\end{ttdescription}
 
 \medskip Theory and {\ML} files are located by skimming through the
 directories listed in Isabelle's internal load path, which merely contains the
@@ -83,133 +52,18 @@
 
 \subsection{*Theory inclusion}
 \begin{ttbox}
-subthy      : theory * theory -> bool
-eq_thy      : theory * theory -> bool
 transfer    : theory -> thm -> thm
-transfer_sg : Sign.sg -> thm -> thm
 \end{ttbox}
 
-Inclusion and equality of theories is determined by unique
-identification stamps that are created when declaring new components.
-Theorems contain a reference to the theory (actually to its signature)
-they have been derived in.  Transferring theorems to super theories
-has no logical significance, but may affect some operations in subtle
-ways (e.g.\ implicit merges of signatures when applying rules, or
-pretty printing of theorems).
+Transferring theorems to super theories has no logical significance,
+but may affect some operations in subtle ways (e.g.\ implicit merges
+of signatures when applying rules, or pretty printing of theorems).
 
 \begin{ttdescription}
 
-\item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$
-  is included in $thy@2$ wrt.\ identification stamps.
-
-\item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$
-  is exactly the same as $thy@2$.
-
 \item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to
   theory $thy$, provided the latter includes the theory of $thm$.
   
-\item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to
-  \texttt{transfer}, but identifies the super theory via its
-  signature.
-
-\end{ttdescription}
-
-
-\subsection{*Primitive theories}
-\begin{ttbox}
-ProtoPure.thy  : theory
-Pure.thy       : theory
-CPure.thy      : theory
-\end{ttbox}
-\begin{description}
-\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},
-  \ttindexbold{CPure.thy}] contain the syntax and signature of the
-  meta-logic.  There are basically no axioms: meta-level inferences
-  are carried out by \ML\ functions.  \texttt{Pure} and \texttt{CPure}
-  just differ in their concrete syntax of prefix function application:
-  $t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in
-  \texttt{CPure}.  \texttt{ProtoPure} is their common parent,
-  containing no syntax for printing prefix applications at all!
-
-%% FIXME
-%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
-%  the theory $thy$ with new types, constants, etc.  $T$ identifies the theory
-%  internally.  When a theory is redeclared, say to change an incorrect axiom,
-%  bindings to the old axiom may persist.  Isabelle ensures that the old and
-%  new theories are not involved in the same proof.  Attempting to combine
-%  different theories having the same name $T$ yields the fatal error
-%extend_theory  : theory -> string -> \(\cdots\) -> theory
-%\begin{ttbox}
-%Attempt to merge different versions of theory: \(T\)
-%\end{ttbox}
-\end{description}
-
-%% FIXME
-%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
-%      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
-%\hfill\break   %%% include if line is just too short
-%is the \ML{} equivalent of the following theory definition:
-%\begin{ttbox}
-%\(T\) = \(thy\) +
-%classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
-%        \dots
-%default {\(d@1,\dots,d@r\)}
-%types   \(tycon@1\),\dots,\(tycon@i\) \(n\)
-%        \dots
-%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
-%        \dots
-%consts  \(b@1\),\dots,\(b@k\) :: \(\tau\)
-%        \dots
-%rules   \(name\) \(rule\)
-%        \dots
-%end
-%\end{ttbox}
-%where
-%\begin{tabular}[t]{l@{~=~}l}
-%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
-%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
-%$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
-%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
-%\\
-%$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
-%$rules$   & \tt[("$name$",$rule$),\dots]
-%\end{tabular}
-
-
-\subsection{Inspecting a theory}\label{sec:inspct-thy}
-\index{theories!inspecting|bold}
-\begin{ttbox}
-print_syntax        : theory -> unit
-print_theory        : theory -> unit
-parents_of          : theory -> theory list
-ancestors_of        : theory -> theory list
-sign_of             : theory -> Sign.sg
-Sign.stamp_names_of : Sign.sg -> string list
-\end{ttbox}
-These provide means of viewing a theory's components.
-\begin{ttdescription}
-\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$
-  (grammar, macros, translation functions etc., see
-  page~\pageref{pg:print_syn} for more details).
-  
-\item[\ttindexbold{print_theory} $thy$] prints the logical parts of
-  $thy$, excluding the syntax.
-  
-\item[\ttindexbold{parents_of} $thy$] returns the direct ancestors
-  of~$thy$.
-  
-\item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$
-  (not including $thy$ itself).
-  
-\item[\ttindexbold{sign_of} $thy$] returns the signature associated
-  with~$thy$.  It is useful with functions like {\tt
-    read_instantiate_sg}, which take a signature as an argument.
-  
-\item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures}
-  returns the names of the identification \rmindex{stamps} of ax
-  signature.  These coincide with the names of its full ancestry
-  including that of $sg$ itself.
-
 \end{ttdescription}