doc-src/Ref/theories.tex

+
 %% $Id$
 
 \chapter{Theories, Terms and Types} \label{theories}
 \index{theories|(}\index{signatures|bold}
 \index{reading!axioms|see{{\tt assume_ax}}} Theories organize the

 \item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
   informs Isabelle that theory $thyname$ no longer exists.  If you delete the
   theory files for $thyname$ then you must execute {\tt unlink_thy};
   otherwise {\tt update} will complain about a missing file.
 \end{ttdescription}
-
-
-%FIXME remove
-%\goodbreak
-%\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
-%The theory mechanism depends upon reference variables.  At the end of a
-%Poly/\ML{} session, the contents of references are lost unless they are
-%declared in the current database.  In particular, assignments to references
-%of the {\tt Pure} database are lost, including all information about loaded
-%theories. To avoid losing this information simply call
-%\begin{ttbox}
-%init_thy_reader();
-%\end{ttbox}
-%when building the new database.
 
 
 \subsection{*Pseudo theories}\label{sec:pseudo-theories}
 \indexbold{theories!pseudo}%
 Any automatic reloading facility requires complete knowledge of all

 \item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
 returns the identification \rmindex{stamps} of the signature associated
 with~$thy$.
 \end{ttdescription}
 
-%FIXME move to sysman!
-%\section{Generating HTML documents}
-%\index{HTML|bold} 
-%
-%Isabelle is able to make HTML documents that show a theory's
-%definition, the theorems proved in its ML file and the relationship
-%with its ancestors and descendants. HTML stands for Hypertext Markup
-%Language and is used in the World Wide Web to represent text
-%containing images and links to other documents. Web browsers like
-%{\tt xmosaic} or {\tt netscape} are used to view these documents.
-%
-%Besides the three HTML files that are made for every theory
-%(definition and theorems, ancestors, descendants), Isabelle stores
-%links to all theories in an index file. These indexes are themself
-%linked with other indexes to represent the hierarchic structure of
-%Isabelle's logics.
-%
-%To make HTML files for logics that are part of the Isabelle
-%distribution, simply set the shell environment variable {\tt
-%MAKE_HTML} before compiling a logic. This works for single logics as
-%well as for the shell script {\tt make-all} (see
-%\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
-%{\tt csh} style shell, the following commands can be used:
-%
-%\begin{ttbox}
-%cd FOL
-%setenv MAKE_HTML
-%make
-%\end{ttbox}
-%
-%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
-%database is used to manually load a theory.
-%
-%As you will see below, the HTML generation is controlled by a boolean
-%reference variable. If you want to make databases which define this
-%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
-%MAKE_HTML} to ``{\tt true}'':
-%
-%\begin{ttbox}
-%cd FOL
-%setenv MAKE_HTML true
-%make
-%\end{ttbox}
-%
-%All theories loaded from within the {\tt FOL} database and all
-%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
-%the boolean reference variable {\tt make_html}. Be careful when making
-%such databases publicly available since it means that your users will
-%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
-%{\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
-%logic do not exist. Otherwise some of the hypertext links might point
-%to non-existing documents.
-%
-%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
-%distribution package at
-%
-%\begin{ttbox}
-%http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
-%\end{ttbox}
-%
-%
-%\subsection*{Manual HTML generation}
-%
-%To manually control the generation of HTML files the following
-%commands and reference variables are used:
-%
-%\begin{ttbox}
-%init_html   : unit -> unit
-%make_html   : bool ref
-%finish_html : unit -> unit
-%\end{ttbox}
-%
-%\begin{ttdescription}
-%\item[\ttindexbold{init_html}]
-%activates the HTML facility. It stores the current working directory
-%as the place where the {\tt index.html} file for all theories loaded
-%afterwards will be stored.
-%
-%\item[\ttindexbold{make_html}]
-%is a boolean reference variable read by {\tt use_thy} and other
-%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
-%to temporarily disable HTML generation.
-%
-%\item[\ttindexbold{finish_html}]
-%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
-%file with information about the theories read since the last use of
-%{\tt init_html} and makes the {\tt index.html} file. If {\tt
-%make_html} is {\tt false} nothing is done.
-%
-%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
-%stored. If there's a {\tt README.html} file it is used instead of
-%{\tt README}.
-%
-%\end{ttdescription}
-%
-%The above functions could be used in the following way:
-%
-%\begin{ttbox}
-%init_html();
-%{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
-%use_thy "List";
-%\dots
-%finish_html();
-%\end{ttbox}
-%
-%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
-%links to theories that were read with a {\tt false} {\tt make_html}
-%and therefore point to non-existing files.
-%
-%
-%\subsection*{Extending or adding a logic}
-%
-%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
-%directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
-%it. This is automatically done if you use
-%
-%\begin{ttbox}\index{use_dir}
-%use_dir : string -> unit
-%\end{ttbox}
-%
-%This function takes a path as its parameter, changes the working
-%directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
-%executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
-%index.html} file written in this directory will be automatically
-%linked to the first index found in the (recursively searched)
-%superdirectories.
-%
-%Instead of adding something like
-%
-%\begin{ttbox}
-%use"ex/ROOT.ML";
-%\end{ttbox}
-%
-%to the logic's makefile you have to use this:
-%
-%\begin{ttbox}
-%use_dir"ex";
-%\end{ttbox}
-%
-%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
-%reference variable has. It can either be inherited from the used \ML{}
-%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
-%MAKE_HTML}.
-%
-%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},
-%or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
-%is a hypertext link to the whole \ML{} file.
-%
-%You can add section headings to the list of theorems by using
-%
-%\begin{ttbox}\index{use_dir}
-%section: string -> unit
-%\end{ttbox}
-%
-%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
-%one of the above functions. If {\tt make_html} is {\tt false} nothing
-%is done.
-%
-%
-%\subsection*{Using someone else's database}
-%
-%To make them independent from their storage place, the HTML files only
-%contain relative paths which are derived from absolute ones like the
-%current working directory, {\tt gif_path} or {\tt base_path}. The
-%latter two are reference variables which are initialized at the time
-%when the {\tt Pure} database is made. Because you need write access
-%for the current directory to make HTML files and therefore (probably)
-%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
-%from it.
-%
-%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
-%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
-%files will still be usable but may contain incomplete titles and lack
-%some hypertext links.
-%
-%It's also a good idea to set {\tt gif_path} which points to the
-%directory containing two GIF images used in the HTML
-%documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
-%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
-%changing the location of the HTML files (as they contain relative
-%paths) and also causes trouble if the database's maker (re)moves the
-%GIFs.
-%
-%Here's what you should do before invoking {\tt init_html} using
-%someone else's \ML{} database:
-%
-%\begin{ttbox}
-%base_path := "/home/smith/isabelle";
-%gif_path := "/home/smith/isabelle/Tools";
-%init_html();
-%\dots
-%\end{ttbox}
-
 
 \section{Terms}
 \index{terms|bold}
 Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
 with six constructors: