\index{reading!axioms|see{{\tt assume_ax}}}

 \index{reading!axioms|see{{\tt assume_ax}}} Theories organize the

 Theories organize the syntax, declarations and axioms of a mathematical

 syntax, declarations and axioms of a mathematical development.  They

 development.  They are built, starting from the Pure theory, by extending

 are built, starting from the {\Pure} or {\CPure} theory, by extending

 and merging existing theories.  They have the \ML\ type \mltydx{theory}.

 and merging existing theories.  They have the \ML\ type

 Theory operations signal errors by raising exception \xdx{THEORY},

 \mltydx{theory}.  Theory operations signal errors by raising exception

 returning a message and a list of theories.

 \xdx{THEORY}, returning a message and a list of theories.

 \item[{\it theoryDef}]

 \item[{\it theoryDef}] is the full definition.  The new theory is

   is the full definition.  The new theory is called $id$.  It is the union

   called $id$.  It is the union of the named {\bf parent

   of the named {\bf parent theories}\indexbold{theories!parent}, possibly

     theories}\indexbold{theories!parent}, possibly extended with new

   extended with new classes, etc.  The basic theory, which contains only

   components.  \thydx{Pure} and \thydx{CPure} are the basic theories,

   the meta-logic, is called \thydx{Pure}.

   which contain only the meta-logic. They differ just in their

   concrete syntax for function applications.

 \item[$sort$]

 \item[$sort$] is a finite set of classes.  A single class $id$

   is a finite set of classes.  A single class $id$ abbreviates the singleton

   abbreviates the sort $\ttlbrace id\ttrbrace$.

   set {\tt\{}$id${\tt\}}.

   ('a,'b)~"*"~(infixr~20)}, which expresses binary product types.

   ('a,'b)~"*"~(infixr~20)}, which may express binary product types.

 \item[$arities$]

 \item[$arities$] is a series of type arity declarations.  Each assigns

   is a series of arity declarations.  Each assigns arities to type

   arities to type constructors.  The $name$ must be an existing type

   constructors.  The $name$ must be an existing type constructor, which is

   constructor, which is given the additional arity $arity$.

   given the additional arity $arity$.

 \item[$consts$] is a series of constant declarations.  Each new

 \item[$constDecl$]

   constant $name$ is given the specified type.  The optional $mixfix$

   is a series of constant declarations.  Each new constant $name$ is given

   annotations may attach concrete syntax to the constant.

   the specified type.  The optional $mixfix$ annotations may

   attach concrete syntax to the constant. A variant of {\tt consts} is the

 \item[$syntax$] \index{*syntax section}\index{print mode} is a variant

   {\tt syntax} section\index{*syntax section}, which adds just syntax without

   of $consts$ which adds just syntax without actually declaring

   declaring logical constants.

   logical constants.  This gives full control over a theory's context

   free grammar. The optional $mode$ specifies the print mode where the

   mixfix productions should be added. If there is no \texttt{output}

   option given, all productions are also added to the input syntax

   (regardless of the print mode).

   theory file.

   theory.

 {\bf Definitions} are intended to express abbreviations. The simplest form of

 {\bf Definitions} are intended to express abbreviations. The simplest

 a definition is $f \equiv t$, where $f$ is a constant. Isabelle also allows a

 form of a definition is $f \equiv t$, where $f$ is a constant.

 derived form where the arguments of~$f$ appear on the left, abbreviating a

 Isabelle also allows a derived forms where the arguments of~$f$ appear

 string of $\lambda$-abstractions.

 on the left, abbreviating a string of $\lambda$-abstractions.

 \item Arguments (on the left-hand side) must be distinct variables

 \item Arguments (on the left-hand side) must be distinct variables.

 \item All type variables on the right-hand side must also appear on the

 \item All type variables on the right-hand side must also appear on

   left-hand side; this prohibits definitions such as {\tt zero == length []}.

   the left-hand side; this prohibits definitions such as {\tt

     (zero::nat) == length ([]::'a list)}.

 \item There must be no two declarations $ty :: (\vec{r})c$ and $ty ::

 \item There must not be any two declarations $ty :: (\vec{r})c$ and

   (\vec{s})c$ with $\vec{r} \neq \vec{s}$.  For example, the following is

   $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$.  For example, this

   forbidden:

   excludes the following:

 \begin{ttbox}

 \begin{ttbox}

 types

   'a ty

   ty :: ({\ttlbrace}logic{\ttrbrace}) logic

   foo :: ({\ttlbrace}logic{\ttrbrace}) logic

   ty :: ({\ttlbrace}{\ttrbrace})logic

   foo :: ({\ttlbrace}{\ttrbrace})logic

 expresses that the set of types represented by $s'$ is a subset of the set of

 expresses that the set of types represented by $s'$ is a subset of the

 types represented by $s$.  For example, the following is forbidden:

 set of types represented by $s$.  Assuming $term \preceq logic$, the

 \begin{ttbox}

 following is forbidden:

 classes

 \begin{ttbox}

   term < logic

 types

   'a ty

   ty :: ({\ttlbrace}logic{\ttrbrace})logic

   foo :: ({\ttlbrace}logic{\ttrbrace})logic

   ty :: ({\ttlbrace}{\ttrbrace})term

   foo :: ({\ttlbrace}{\ttrbrace})term

 Each theory definition must reside in a separate file.  Let the file {\it

 Each theory definition must reside in a separate file.  Let the file

   T}{\tt.thy} contain the definition of a theory called~$T$, whose parent

 {\it T}{\tt.thy} contain the definition of a theory called~$T$, whose

 theories are $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"{\it

 parent theories are $TB@1$ \dots $TB@n$.  Calling

   T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{}

 \ttindex{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy},

 file {\tt.{\it T}.thy.ML}, and reads the latter file.  Recursive {\tt

 writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the

   use_thy} calls load those parent theories that have not been loaded

 latter file.  Recursive {\tt use_thy} calls load those parent theories

 previously; the recursive calls may continue to any depth.  One {\tt use_thy}

 that have not been loaded previously; the recursive calls may continue

 call can read an entire logic provided all theories are linked appropriately.

 to any depth.  One {\tt use_thy} call can read an entire logic

 provided all theories are linked appropriately.

 Finally the file {\it T}{\tt.ML} is read, if it exists.  This file normally

 Finally the file {\it T}{\tt.ML} is read, if it exists.  Since the

 begins with the declaration {\tt open~$T$} and contains proofs involving

 structure $T$ is automatically open in this context, proof scripts may

 the new theory.

 (or even should) refer to its components by unqualified names.

 \goodbreak

 %FIXME remove

 \subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}

 %\goodbreak

 The theory mechanism depends upon reference variables.  At the end of a

 %\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}

 Poly/\ML{} session, the contents of references are lost unless they are

 %The theory mechanism depends upon reference variables.  At the end of a

 declared in the current database.  In particular, assignments to references

 %Poly/\ML{} session, the contents of references are lost unless they are

 of the {\tt Pure} database are lost, including all information about loaded

 %declared in the current database.  In particular, assignments to references

 theories. To avoid losing this information simply call

 %of the {\tt Pure} database are lost, including all information about loaded

 \begin{ttbox}

 %theories. To avoid losing this information simply call

 init_thy_reader();

 %\begin{ttbox}

 \end{ttbox}

 %init_thy_reader();

 when building the new database.

 %\end{ttbox}

 %when building the new database.

 For an extensive example of how this technique can be used to link lots of

 For an extensive example of how this technique can be used to link

 theory files and load them by just a few {\tt use_thy} calls, consult the

 lots of theory files and load them by just a few {\tt use_thy} calls

 sources of \ZF{} set theory.

 see the sources of one of the major object-logics (e.g.\ \ZF).

 \subsection{Building a theory}

 \subsection{*Building a theory}

 pure_thy       : theory

 Pure.thy       : theory

 CPure.thy      : theory

 \begin{ttdescription}

 \begin{description}

 \item[\ttindexbold{pure_thy}] contains just the syntax and signature

 \item[\ttindexbold{Pure.thy}, \ttindexbold{CPure.thy}] contain the

   of the meta-logic.  There are no axioms: meta-level inferences are carried

   syntax and signature of the meta-logic.  There are no axioms:

   out by \ML\ functions.

   meta-level inferences are carried out by \ML\ functions. The two

   \Pure s just differ in their concrete syntax of function

   application: $t(u@1, \ldots, u@n)$ vs.\ $t\,u@1,\ldots\,u@n$.

 \end{ttdescription}

 \end{description}

 \item[\ttindexbold{print_theory} $thy$]

 \item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$

 prints the contents of $thy$ excluding the syntax related parts (which are

   (grammar, macros, translation functions etc., see

 shown by {\tt print_syntax}).  The output is quite verbose.

   page~\pageref{pg:print_syn} for more details).

 \item[\ttindexbold{print_theory} $thy$] prints the logical parts of

   $thy$, excluding the syntax.

 %FIXME move to sysman!

 \section{Generating HTML documents}

 %\section{Generating HTML documents}

 \index{HTML|bold} 

 %\index{HTML|bold} 

 %

 Isabelle is able to make HTML documents that show a theory's

 %Isabelle is able to make HTML documents that show a theory's

 definition, the theorems proved in its ML file and the relationship

 %definition, the theorems proved in its ML file and the relationship

 with its ancestors and descendants. HTML stands for Hypertext Markup

 %with its ancestors and descendants. HTML stands for Hypertext Markup

 Language and is used in the World Wide Web to represent text

 %Language and is used in the World Wide Web to represent text

 containing images and links to other documents. Web browsers like

 %containing images and links to other documents. Web browsers like

 {\tt xmosaic} or {\tt netscape} are used to view these documents.

 %{\tt xmosaic} or {\tt netscape} are used to view these documents.

 %

 Besides the three HTML files that are made for every theory

 %Besides the three HTML files that are made for every theory

 (definition and theorems, ancestors, descendants), Isabelle stores

 %(definition and theorems, ancestors, descendants), Isabelle stores

 links to all theories in an index file. These indexes are themself

 %links to all theories in an index file. These indexes are themself

 linked with other indexes to represent the hierarchic structure of

 %linked with other indexes to represent the hierarchic structure of

 Isabelle's logics.

 %Isabelle's logics.

 %

 To make HTML files for logics that are part of the Isabelle

 %To make HTML files for logics that are part of the Isabelle

 distribution, simply set the shell environment variable {\tt

 %distribution, simply set the shell environment variable {\tt

 MAKE_HTML} before compiling a logic. This works for single logics as

 %MAKE_HTML} before compiling a logic. This works for single logics as

 well as for the shell script {\tt make-all} (see

 %well as for the shell script {\tt make-all} (see

 \ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a

 %\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a

 {\tt csh} style shell, the following commands can be used:

 %{\tt csh} style shell, the following commands can be used:

 %

 \begin{ttbox}

 %\begin{ttbox}

 cd FOL

 %cd FOL

 setenv MAKE_HTML

 %setenv MAKE_HTML

 make

 %make

 \end{ttbox}

 %\end{ttbox}

 %

 The databases made this way do not differ from the ones made with an

 %The databases made this way do not differ from the ones made with an

 unset {\tt MAKE_HTML}; in particular no HTML files are written if the

 %unset {\tt MAKE_HTML}; in particular no HTML files are written if the

 database is used to manually load a theory.

 %database is used to manually load a theory.

 %

 As you will see below, the HTML generation is controlled by a boolean

 %As you will see below, the HTML generation is controlled by a boolean

 reference variable. If you want to make databases which define this

 %reference variable. If you want to make databases which define this

 variable's value as {\tt true} and where therefore HTML files are

 %variable's value as {\tt true} and where therefore HTML files are

 written each time {\tt use_thy} is invoked, you have to set {\tt

 %written each time {\tt use_thy} is invoked, you have to set {\tt

 MAKE_HTML} to ``{\tt true}'':

 %MAKE_HTML} to ``{\tt true}'':

 %

 \begin{ttbox}

 %\begin{ttbox}

 cd FOL

 %cd FOL

 setenv MAKE_HTML true

 %setenv MAKE_HTML true

 make

 %make

 \end{ttbox}

 %\end{ttbox}

 %

 All theories loaded from within the {\tt FOL} database and all

 %All theories loaded from within the {\tt FOL} database and all

 databases derived from it will now cause HTML files to be written.

 %databases derived from it will now cause HTML files to be written.

 This behaviour can be changed by assigning a value of {\tt false} to

 %This behaviour can be changed by assigning a value of {\tt false} to

 the boolean reference variable {\tt make_html}. Be careful when making

 %the boolean reference variable {\tt make_html}. Be careful when making

 such databases publicly available since it means that your users will

 %such databases publicly available since it means that your users will

 generate HTML files though they might not intend to do so.

 %generate HTML files though they might not intend to do so.

 %

 As some of Isabelle's logics are based on others (e.g. {\tt ZF} on

 %As some of Isabelle's logics are based on others (e.g. {\tt ZF} on

 {\tt FOL}) and because the HTML files list a theory's ancestors, you

 %{\tt FOL}) and because the HTML files list a theory's ancestors, you

 should not make HTML files for a logic if the HTML files for the base

 %should not make HTML files for a logic if the HTML files for the base

 logic do not exist. Otherwise some of the hypertext links might point

 %logic do not exist. Otherwise some of the hypertext links might point

 to non-existing documents.

 %to non-existing documents.

 %

 The entry point to all logics is the {\tt index.html} file located in

 %The entry point to all logics is the {\tt index.html} file located in

 Isabelle's main directory. You can also access a HTML version of the

 %Isabelle's main directory. You can also access a HTML version of the

 distribution package at

 %distribution package at

 %

 \begin{ttbox}

 %\begin{ttbox}

 http://www4.informatik.tu-muenchen.de/~nipkow/isabelle

 %http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/

 \end{ttbox}

 %\end{ttbox}

 %

 %

 \subsection*{Manual HTML generation}

 %\subsection*{Manual HTML generation}

 %

 To manually control the generation of HTML files the following

 %To manually control the generation of HTML files the following

 commands and reference variables are used:

 %commands and reference variables are used:

 %

 \begin{ttbox}

 %\begin{ttbox}

 init_html   : unit -> unit

 %init_html   : unit -> unit

 make_html   : bool ref

 %make_html   : bool ref

 finish_html : unit -> unit

 %finish_html : unit -> unit

 \end{ttbox}

 %\end{ttbox}

 %

 \begin{ttdescription}

 %\begin{ttdescription}

 \item[\ttindexbold{init_html}]

 %\item[\ttindexbold{init_html}]

 activates the HTML facility. It stores the current working directory

 %activates the HTML facility. It stores the current working directory

 as the place where the {\tt index.html} file for all theories loaded

 %as the place where the {\tt index.html} file for all theories loaded

 afterwards will be stored.

 %afterwards will be stored.

 %

 \item[\ttindexbold{make_html}]

 %\item[\ttindexbold{make_html}]

 is a boolean reference variable read by {\tt use_thy} and other

 %is a boolean reference variable read by {\tt use_thy} and other

 functions to decide whether HTML files should be made. After you have

 %functions to decide whether HTML files should be made. After you have

 used {\tt init_html} you can manually change {\tt make_html}'s value

 %used {\tt init_html} you can manually change {\tt make_html}'s value

 to temporarily disable HTML generation.

 %to temporarily disable HTML generation.

 %

 \item[\ttindexbold{finish_html}]

 %\item[\ttindexbold{finish_html}]

 has to be called after all theories have been read that should be

 %has to be called after all theories have been read that should be

 listed in the current {\tt index.html} file. It reads a temporary

 %listed in the current {\tt index.html} file. It reads a temporary

 file with information about the theories read since the last use of

 %file with information about the theories read since the last use of

 {\tt init_html} and makes the {\tt index.html} file. If {\tt

 %{\tt init_html} and makes the {\tt index.html} file. If {\tt

 make_html} is {\tt false} nothing is done.

 %make_html} is {\tt false} nothing is done.

 %

 The indexes made by this function also contain a link to the {\tt

 %The indexes made by this function also contain a link to the {\tt

 README} file if there exists one in the directory where the index is

 %README} file if there exists one in the directory where the index is

 stored. If there's a {\tt README.html} file it is used instead of

 %stored. If there's a {\tt README.html} file it is used instead of

 {\tt README}.

 %{\tt README}.

 %

 \end{ttdescription}

 %\end{ttdescription}

 %

 The above functions could be used in the following way:

 %The above functions could be used in the following way:

 %

 \begin{ttbox}

 %\begin{ttbox}

 init_html();

 %init_html();

 {\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}

 %{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}

 use_thy "List";

 %use_thy "List";

 \dots

 %\dots

 finish_html();

 %finish_html();

 \end{ttbox}

 %\end{ttbox}

 %

 Please note that HTML files are made only for those theories that are

 %Please note that HTML files are made only for those theories that are

 read while {\tt make_html} is {\tt true}. These files may contain

 %read while {\tt make_html} is {\tt true}. These files may contain

 links to theories that were read with a {\tt false} {\tt make_html}

 %links to theories that were read with a {\tt false} {\tt make_html}

 and therefore point to non-existing files.

 %and therefore point to non-existing files.

 %

 %

 \subsection*{Extending or adding a logic}

 %\subsection*{Extending or adding a logic}

 %

 If you add a new subdirectory to Isabelle's logics (or add a completly

 %If you add a new subdirectory to Isabelle's logics (or add a completly

 new logic), you would have to call {\tt init_html} at the start of every

 %new logic), you would have to call {\tt init_html} at the start of every

 directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of

 %directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of

 it. This is automatically done if you use

 %it. This is automatically done if you use

 %

 \begin{ttbox}\index{use_dir}

 %\begin{ttbox}\index{use_dir}

 use_dir : string -> unit

 %use_dir : string -> unit

 \end{ttbox}

 %\end{ttbox}

 %

 This function takes a path as its parameter, changes the working

 %This function takes a path as its parameter, changes the working

 directory, calls {\tt init_html} if {\tt make_html} is {\tt true},

 %directory, calls {\tt init_html} if {\tt make_html} is {\tt true},

 executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt

 %executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt

 index.html} file written in this directory will be automatically

 %index.html} file written in this directory will be automatically

 linked to the first index found in the (recursively searched)

 %linked to the first index found in the (recursively searched)

 superdirectories.

 %superdirectories.

 %

 Instead of adding something like

 %Instead of adding something like

 %

 \begin{ttbox}

 %\begin{ttbox}

 use"ex/ROOT.ML";

 %use"ex/ROOT.ML";

 \end{ttbox}

 %\end{ttbox}

 %

 to the logic's makefile you have to use this:

 %to the logic's makefile you have to use this:

 %

 \begin{ttbox}

 %\begin{ttbox}

 use_dir"ex";

 %use_dir"ex";

 \end{ttbox}

 %\end{ttbox}

 %

 Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is

 %Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is

 {\tt true} the generation of HTML files depends on the value this

 %{\tt true} the generation of HTML files depends on the value this

 reference variable has. It can either be inherited from the used \ML{}

 %reference variable has. It can either be inherited from the used \ML{}

 database or set in the makefile before {\tt use_dir} is invoked,

 %database or set in the makefile before {\tt use_dir} is invoked,

 e.g. to set it's value according to the environment variable {\tt

 %e.g. to set it's value according to the environment variable {\tt

 MAKE_HTML}.

 %MAKE_HTML}.

 %

 The generated HTML files contain all theorems that were proved in the

 %The generated HTML files contain all theorems that were proved in the

 theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},

 %theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},

 or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there

 %or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there

 is a hypertext link to the whole \ML{} file.

 %is a hypertext link to the whole \ML{} file.

 %

 You can add section headings to the list of theorems by using

 %You can add section headings to the list of theorems by using

 %

 \begin{ttbox}\index{use_dir}

 %\begin{ttbox}\index{use_dir}

 section: string -> unit

 %section: string -> unit

 \end{ttbox}

 %\end{ttbox}

 %

 in a theory's ML file, which converts a plain string to a HTML

 %in a theory's ML file, which converts a plain string to a HTML

 heading and inserts it before the next theorem proved or stored with

 %heading and inserts it before the next theorem proved or stored with

 one of the above functions. If {\tt make_html} is {\tt false} nothing

 %one of the above functions. If {\tt make_html} is {\tt false} nothing

 is done.

 %is done.

 %

 %

 \subsection*{Using someone else's database}

 %\subsection*{Using someone else's database}

 %

 To make them independent from their storage place, the HTML files only

 %To make them independent from their storage place, the HTML files only

 contain relative paths which are derived from absolute ones like the

 %contain relative paths which are derived from absolute ones like the

 current working directory, {\tt gif_path} or {\tt base_path}. The

 %current working directory, {\tt gif_path} or {\tt base_path}. The

 latter two are reference variables which are initialized at the time

 %latter two are reference variables which are initialized at the time

 when the {\tt Pure} database is made. Because you need write access

 %when the {\tt Pure} database is made. Because you need write access

 for the current directory to make HTML files and therefore (probably)

 %for the current directory to make HTML files and therefore (probably)

 generate them in your home directory, the absolute {\tt base_path} is

 %generate them in your home directory, the absolute {\tt base_path} is

 not correct if you use someone else's database or a database derived

 %not correct if you use someone else's database or a database derived

 from it.

 %from it.

 %

 In that case you first should set {\tt base_path} to the value of {\em

 %In that case you first should set {\tt base_path} to the value of {\em

 your} Isabelle main directory, i.e. the directory that contains the

 %your} Isabelle main directory, i.e. the directory that contains the

 subdirectories where standard logics like {\tt FOL} and {\tt HOL} or

 %subdirectories where standard logics like {\tt FOL} and {\tt HOL} or

 your own logics are stored. If you do not do this, the generated HTML

 %your own logics are stored. If you do not do this, the generated HTML

 files will still be usable but may contain incomplete titles and lack

 %files will still be usable but may contain incomplete titles and lack

 some hypertext links.

 %some hypertext links.

 %

 It's also a good idea to set {\tt gif_path} which points to the

 %It's also a good idea to set {\tt gif_path} which points to the

 directory containing two GIF images used in the HTML

 %directory containing two GIF images used in the HTML

 documents. Normally this is the {\tt Tools} subdirectory of Isabelle's

 %documents. Normally this is the {\tt Tools} subdirectory of Isabelle's

 main directory. While its value in general is still valid, your HTML

 %main directory. While its value in general is still valid, your HTML

 files would depend on files not owned by you. This prevents you from

 %files would depend on files not owned by you. This prevents you from

 changing the location of the HTML files (as they contain relative

 %changing the location of the HTML files (as they contain relative

 paths) and also causes trouble if the database's maker (re)moves the

 %paths) and also causes trouble if the database's maker (re)moves the

 GIFs.

 %GIFs.

 %

 Here's what you should do before invoking {\tt init_html} using

 %Here's what you should do before invoking {\tt init_html} using

 someone else's \ML{} database:

 %someone else's \ML{} database:

 %

 \begin{ttbox}

 %\begin{ttbox}

 base_path := "/home/smith/isabelle";

 %base_path := "/home/smith/isabelle";

 gif_path := "/home/smith/isabelle/Tools";

 %gif_path := "/home/smith/isabelle/Tools";

 init_html();

 %init_html();

 \dots

 %\dots

 \end{ttbox}

 %\end{ttbox}

 with six constructors: there are six kinds of term.

 with six constructors:

 rep_cterm  : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}

 rep_cterm  : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace

 rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}

 rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace

   theory files.  A theory can have at most one oracle.

   theory files.  Any theory node can have at most one oracle.