# HG changeset patch # User wenzelm # Date 925810045 -7200 # Node ID 971f238ef3ec9e2146756cb1aae4d6b6f5f0244d # Parent a7d7985050a93d845e2a9fbbc2328099683471fc tuned; diff -r a7d7985050a9 -r 971f238ef3ec doc-src/Ref/introduction.tex --- a/doc-src/Ref/introduction.tex Tue May 04 10:26:00 1999 +0200 +++ b/doc-src/Ref/introduction.tex Tue May 04 11:27:25 1999 +0200 @@ -44,6 +44,8 @@ isabellehome \rangle\)/bin/isabelle}, though! See \texttt{isatool install} in \emph{The Isabelle System Manual} of how to do this properly.} +\medskip + The object-logic image to load may be also specified explicitly as an argument to the {\tt isabelle} command, e.g. \begin{ttbox} @@ -76,7 +78,7 @@ \medskip Saving the {\ML} state is not enough. Record, on a file, the top-level commands that generate your theories and proofs. Such a record allows you to replay the proofs whenever required, for instance after making -minor changes to the axioms. Ideally, your these sources will be somewhat +minor changes to the axioms. Ideally, these sources will be somewhat intelligible to others as a formal description of your work. It is good practice to put all source files that constitute a separate @@ -84,7 +86,7 @@ called \texttt{ROOT.ML} that contains appropriate commands to load all other files required. Running \texttt{isabelle} with option \texttt{-u} automatically loads \texttt{ROOT.ML} on entering the session. The -\texttt{isatool usedir} utility provides some more options to manage your +\texttt{isatool usedir} utility provides some more options to manage Isabelle sessions, such as automatic generation of theory browsing information. \medskip More details about the \texttt{isabelle} and \texttt{isatool} @@ -145,7 +147,8 @@ commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are expanded appropriately. Note that \texttt{\~\relax} abbreviates \texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates -\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}. +\texttt{\$ISABELLE_HOME}\index{*\$ISABELLE_HOME}. The syntax for path +specifications follows Unix conventions. \section{Reading theories}\label{sec:intro-theories} @@ -181,10 +184,11 @@ the internal database of loaded theories, raising an error if absent. \item[\ttindexbold{use_thy} "$name$";] reads theory $name$ from the file - system, looking for $name$\texttt{.thy} and (optionally) $name$\texttt{.ML}; - also makes sure that all parent theories are loaded as well. In case some - older versions have already been present, \texttt{use_thy} only tries to - reload $name$ itself, but is content with any version of its parents. + system, looking for $name$\texttt{.thy} and $name$\texttt{.ML} (the latter + being optional). It also ensures that all parent theories are loaded as + well. In case some older versions have already been present, + \texttt{use_thy} only tries to reload $name$ itself, but is content with any + version of its ancestors. \item[\ttindexbold{time_use_thy} "$name$";] same as \texttt{use_thy}, but reports the time taken to process the actual theory parts and {\ML} files @@ -221,11 +225,10 @@ (\S\ref{sec:goals-printing}). \begin{ttdescription} -\item[\ttindexbold{Pretty.setdepth} \(d\);] - tells Isabelle's pretty printer to limit the printing depth to~$d$. This - affects Isabelle's display of theorems and terms. The default value - is~0, which permits printing to an arbitrary depth. Useful values for - $d$ are~10 and~20. +\item[\ttindexbold{Pretty.setdepth} \(d\);] tells Isabelle's pretty printer to + limit the printing depth to~$d$. This affects the display of theorems and + terms. The default value is~0, which permits printing to an arbitrary + depth. Useful values for $d$ are~10 and~20. \item[\ttindexbold{Pretty.setmargin} \(m\);] tells Isabelle's pretty printer to assume a right margin (page width) diff -r a7d7985050a9 -r 971f238ef3ec doc-src/Ref/ref.ind --- a/doc-src/Ref/ref.ind Tue May 04 10:26:00 1999 +0200 +++ b/doc-src/Ref/ref.ind Tue May 04 11:27:25 1999 +0200 @@ -27,7 +27,7 @@ \item {\tt abstract_over}, \bold{63} \item {\tt abstract_rule}, \bold{49} \item {\tt aconv}, \bold{63} - \item {\tt add_path}, \bold{59} + \item {\tt add_path}, \bold{60} \item {\tt addaltern}, \bold{137} \item {\tt addbefore}, \bold{137} \item {\tt Addcongs}, \bold{107} @@ -189,7 +189,7 @@ \item {\tt cprems_of}, \bold{45} \item {\tt cprop_of}, \bold{44} \item {\tt CPure} theory, 55 - \item {\tt CPure.thy}, \bold{60} + \item {\tt CPure.thy}, \bold{61} \item {\tt crep_thm}, \bold{45} \item {\tt cterm} ML type, 64 \item {\tt cterm_instantiate}, \bold{43} @@ -423,7 +423,6 @@ \item {\tt match_tac}, \bold{21}, 134 \item {\tt max_pri}, 70, \bold{76} \item {\tt merge_ss}, \bold{109} - \item {\tt merge_theories}, \bold{61} \item meta-assumptions, 37, 46, 48, 51 \subitem printing of, 5 \item meta-equality, 47--49 @@ -434,10 +433,10 @@ \subitem in theorems, 43 \item meta-rules, \see{meta-rules}{1}, 46--52 \item {\tt METAHYPS}, 19, \bold{37} - \item mixfix declarations, 56, 75--80 + \item mixfix declarations, 57, 75--80 \item {\tt mk_atomize}, \bold{127} \item {\tt mk_simproc}, \bold{123} - \item {\tt ML} section, 57, 97, 99 + \item {\tt ML} section, 58, 97, 99 \item model checkers, 81 \item {\tt mp} theorem, \bold{143} \item {\tt mp_tac}, \bold{142} @@ -529,7 +528,7 @@ \item {\tt PROP} symbol, 71 \item {\textit {prop}} type, 65, 72 \item {\tt prop} nonterminal, \bold{70}, 82 - \item {\tt ProtoPure.thy}, \bold{60} + \item {\tt ProtoPure.thy}, \bold{61} \item {\tt prove_goal}, 14, \bold{16} \item {\tt prove_goalw}, \bold{16} \item {\tt prove_goalw_cterm}, \bold{16} @@ -540,7 +539,7 @@ \item {\tt pttrn} nonterminal, \bold{72} \item {\tt pttrns} nonterminal, \bold{72} \item {\tt Pure} theory, 55, 70, 74 - \item {\tt Pure.thy}, \bold{60} + \item {\tt Pure.thy}, \bold{61} \item {\tt push_proof}, \bold{17} \item {\tt pwd}, \bold{3} @@ -636,14 +635,14 @@ \item {\tt settermless}, \bold{121} \item {\tt setup} \subitem simplifier, 129 - \subitem theory, 57 + \subitem theory, 58 \item shortcuts \subitem for \texttt{by} commands, 14 \subitem for tactics, 23 \item {\tt show_brackets}, \bold{5} \item {\tt show_consts}, \bold{6} \item {\tt show_hyps}, \bold{5} - \item {\tt show_path}, \bold{59} + \item {\tt show_path}, \bold{60} \item {\tt show_sorts}, \bold{5}, 89, 97 \item {\tt show_tags}, \bold{5} \item {\tt show_types}, \bold{5}, 89, 92, 99 @@ -795,7 +794,6 @@ \subitem taking apart, 44 \item theories, 55--68 \subitem axioms of, 11 - \subitem constructing, \bold{60} \subitem inspecting, \bold{61} \subitem parent, \bold{55} \subitem reading, 3, 59 @@ -838,7 +836,7 @@ \subitem of tactics, 30 \subitem of unification, 46 \item {\tt transfer}, \bold{60} - \item {\tt transfer_sg}, \bold{60} + \item {\tt transfer_sg}, \bold{61} \item {\tt transitive}, \bold{49} \item translations, 96--99 \subitem parse, 80, 88 diff -r a7d7985050a9 -r 971f238ef3ec doc-src/Ref/ref.tex --- a/doc-src/Ref/ref.tex Tue May 04 10:26:00 1999 +0200 +++ b/doc-src/Ref/ref.tex Tue May 04 11:27:25 1999 +0200 @@ -1,5 +1,5 @@ \documentclass[12pt]{report} -\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup} +\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,pdfsetup} %% $Id$ %\includeonly{introduction} @@ -7,7 +7,7 @@ %%% to delete old ones: \\indexbold{\*[^}]*} %% run sedindex ref to prepare index file %%% needs chapter on Provers/typedsimp.ML? -\title{\includegraphics[scale=0.5]{isabelle.eps} \\[4ex] The Isabelle Reference Manual} +\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle Reference Manual} \author{{\em Lawrence C. Paulson}\\ Computer Laboratory \\ University of Cambridge \\ diff -r a7d7985050a9 -r 971f238ef3ec doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Tue May 04 10:26:00 1999 +0200 +++ b/doc-src/Ref/theories.tex Tue May 04 11:27:25 1999 +0200 @@ -27,11 +27,11 @@ \section{Defining theories}\label{sec:ref-defining-theories} -Theories are usually defined using theory definition files (which have a name -suffix {\tt .thy}). There is also a low level interface provided by certain -\ML{} functions (see \S\ref{BuildingATheory}). -Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory -definitions; here is an explanation of the constituent parts: +Theories are defined via theory files $name$\texttt{.thy} (there are also +\ML-level interfaces which are only intended for people building advanced +theory definition packages). Appendix~\ref{app:TheorySyntax} presents the +concrete syntax for theory files; here follows an explanation of the +constituent parts. \begin{description} \item[{\it theoryDef}] is the full definition. The new theory is called $id$. It is the union of the named {\bf parent @@ -39,6 +39,15 @@ components. \thydx{Pure} and \thydx{CPure} are the basic theories, which contain only the meta-logic. They differ just in their concrete syntax for function applications. + + The new theory begins as a merge of its parents. + \begin{ttbox} + Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)" + \end{ttbox} + This error may especially occur when a theory is redeclared --- say to + change an inappropriate definition --- and bindings to old versions persist. + Isabelle ensures that old and new theories of the same name are not involved + in a proof. \item[$classes$] is a series of class declarations. Declaring {\tt$id$ < $id@1$ \dots\ @@ -250,7 +259,8 @@ \item[\ttindexbold{update_thy} "$name$";] is similar to \texttt{use_thy}, but ensures that theory $name$ is fully up-to-date with respect to the file - system --- apart from $name$ itself its parents may be reloaded as well. + system --- apart from $name$ itself any of its ancestors may be reloaded as + well. \item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the internal graph as outdated. While the theory remains usable, subsequent @@ -261,7 +271,7 @@ afterwards. Resetting the \texttt{delete_tmpfiles} flag inhibits this, leaving the generated code for debugging purposes. The basic location for temporary files is determined by the \texttt{ISABELLE_TMP} environment - variable, which is private to the running Isabelle process (it may be + variable (which is private to the running Isabelle process and may be retrieved by \ttindex{getenv} from {\ML}). \end{ttdescription} @@ -279,7 +289,7 @@ \begin{ttdescription} \item[\ttindexbold{show_path}();] displays the load path components in - canonical string representation, which is always according to Unix rules. + canonical string representation (which is always according to Unix rules). \item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning of the load path. @@ -291,11 +301,11 @@ (current directory) only. \end{ttdescription} -In operations referring indirectly to some file, such as -\texttt{use_thy~"$name$"}, the argument may be prefixed by some directory that -will be used as temporary load path. Note that, depending on which parts of -the ancestry of $name$ are already loaded, the dynamic change of paths might -be hard to predict. Use this feature with care only. +In operations referring indirectly to some file, the argument may be prefixed +by a directory that will be used as temporary load path, e.g.\ +\texttt{use_thy~"$dir/name$"}. Note that, depending on which parts of the +ancestry of $name$ are already loaded, the dynamic change of paths might be +hard to predict. Use this feature with care only. \section{Basic operations on theories}\label{BasicOperationsOnTheories} @@ -334,14 +344,11 @@ \end{ttdescription} -\subsection{*Building a theory} -\label{BuildingATheory} -\index{theories!constructing|bold} +\subsection{*Primitive theories} \begin{ttbox} ProtoPure.thy : theory Pure.thy : theory CPure.thy : theory -merge_theories : string -> theory * theory -> theory \end{ttbox} \begin{description} \item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy}, @@ -352,20 +359,14 @@ $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! - -\item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges - the two theories $thy@1$ and $thy@2$, creating a new named theory - node. The resulting theory contains all of the syntax, signature - and axioms of the constituent theories. Merging theories that - contain different identification stamps of the same name fails with - the following message -\begin{ttbox} -Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)" -\end{ttbox} -This error may especially occur when a theory is redeclared --- say to -change an inappropriate definition --- and bindings to old versions -persist. Isabelle ensures that old and new theories of the same name -are not involved in a proof. + +%%FIXME +%\item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges +% the two theories $thy@1$ and $thy@2$, creating a new named theory +% node. The resulting theory contains all of the syntax, signature +% and axioms of the constituent theories. Merging theories that +% contain different identification stamps of the same name fails with +% the following message %% FIXME %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends