summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarRef/logics.tex

changeset 13014 | 3c1c493e6d93 |

parent 12879 | 8e1cae1de136 |

child 13016 | c039b8ede204 |

1.1 --- a/doc-src/IsarRef/logics.tex Mon Mar 04 19:07:22 2002 +0100 1.2 +++ b/doc-src/IsarRef/logics.tex Mon Mar 04 19:07:58 2002 +0100 1.3 @@ -40,12 +40,14 @@ 1.4 \begin{rail} 1.5 'judgment' constdecl 1.6 ; 1.7 - ruleformat ('(' noasm ')')? 1.8 + atomize ('(' 'full' ')')? 1.9 + ; 1.10 + ruleformat ('(' 'noasm' ')')? 1.11 ; 1.12 \end{rail} 1.13 1.14 \begin{descr} 1.15 - 1.16 + 1.17 \item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the 1.18 truth judgment of the current object-logic. Its type $\sigma$ should 1.19 specify a coercion of the category of object-level propositions to $prop$ of 1.20 @@ -53,25 +55,27 @@ 1.21 the object language (internally of syntactic category $logic$) with that of 1.22 $prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any 1.23 theory development. 1.24 - 1.25 + 1.26 \item [$atomize$] (as a method) rewrites any non-atomic premises of a 1.27 sub-goal, using the meta-level equations declared via $atomize$ (as an 1.28 attribute) beforehand. As a result, heavily nested goals become amenable to 1.29 fundamental operations such as resolution (cf.\ the $rule$ method) and 1.30 - proof-by-assumption (cf.\ $assumption$). 1.31 - 1.32 + proof-by-assumption (cf.\ $assumption$). Giving the ``$(full)$'' option 1.33 + here means to turn the subgoal into an object-statement (if possible), 1.34 + including the outermost parameters and assumptions as well. 1.35 + 1.36 A typical collection of $atomize$ rules for a particular object-logic would 1.37 provide an internalization for each of the connectives of $\Forall$, $\Imp$, 1.38 and $\equiv$. Meta-level conjunction expressed in the manner of minimal 1.39 higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$ 1.40 should be covered as well (this is particularly important for locales, see 1.41 \S\ref{sec:locale}). 1.42 - 1.43 + 1.44 \item [$rule_format$] rewrites a theorem by the equalities declared as 1.45 $rulify$ rules in the current object-logic. By default, the result is fully 1.46 normalized, including assumptions and conclusions at any depth. The 1.47 $no_asm$ option restricts the transformation to the conclusion of a rule. 1.48 - 1.49 + 1.50 In common object-logics (HOL, FOL, ZF), the effect of $rule_format$ is to 1.51 replace (bounded) universal quantification ($\forall$) and implication 1.52 ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$. 1.53 @@ -97,21 +101,36 @@ 1.54 \end{rail} 1.55 1.56 \begin{descr} 1.57 + 1.58 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original 1.59 $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but 1.60 also declares type arity $t :: (term, \dots, term) term$, making $t$ an 1.61 actual HOL type constructor. 1.62 + 1.63 \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating 1.64 non-emptiness of the set $A$. After finishing the proof, the theory will be 1.65 - augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL} 1.66 - for more information. Note that user-level theories usually do not directly 1.67 - refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced 1.68 - packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and 1.69 - $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}). 1.70 + augmented by a Gordon/HOL-style type definition, which establishes a 1.71 + bijection between the representing set $A$ and the new type $t$. 1.72 + 1.73 + Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term 1.74 + constant) of the same name. The injection from type to set is called 1.75 + $Rep_t$, its inverse $Abs_t$. Theorems $Rep_t$, $Rep_inverse$, and 1.76 + $Abs_inverse$ provide the most basic characterization as a corresponding 1.77 + injection/surjection pair (in both directions). Rules $Rep_t_inject$ and 1.78 + $Abs_t_inject$ provide a slightly more comfortable view on the injectivity 1.79 + part; likewise do $Rep_t_cases$, $Rep_t_induct$, and $Abs_t_cases$, 1.80 + $Abs_t_induct$ for surjectivity. The latter rules are already declare as 1.81 + type or set rules for the generic $cases$ and $induct$ methods. 1.82 \end{descr} 1.83 1.84 +Raw type declarations are rarely useful in practice. The main application is 1.85 +with experimental (or even axiomatic!) theory fragments. Instead of primitive 1.86 +HOL type definitions, user-level theories usually refer to higher-level 1.87 +packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or 1.88 +$\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}). 1.89 1.90 -\subsection{Low-level tuples} 1.91 + 1.92 +\subsection{Adhoc tuples} 1.93 1.94 \indexisarattof{HOL}{split-format} 1.95 \begin{matharray}{rcl} 1.96 @@ -128,25 +147,89 @@ 1.97 \end{rail} 1.98 1.99 \begin{descr} 1.100 - 1.101 + 1.102 \item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level 1.103 tuple types into canonical form as specified by the arguments given; $\vec 1.104 p@i$ refers to occurrences in premise $i$ of the rule. The 1.105 $split_format~(complete)$ form causes \emph{all} arguments in function 1.106 applications to be represented canonically according to their tuple type 1.107 structure. 1.108 - 1.109 + 1.110 Note that these operations tend to invent funny names for new local 1.111 parameters to be introduced. 1.112 1.113 \end{descr} 1.114 1.115 1.116 -\subsection{Records}\label{sec:hol-record} 1.117 +\section{Records}\label{sec:hol-record} 1.118 + 1.119 +In principle, records merely generalize the concept of tuples where components 1.120 +may be addressed by labels instead of just position. The logical 1.121 +infrastructure of records in Isabelle/HOL is slightly more advanced, though, 1.122 +supporting truly extensible record schemes. This admits operations that are 1.123 +polymorphic with respect to record extension, yielding ``object-oriented'' 1.124 +effects like (single) inheritance. See also \cite{NaraschewskiW-TPHOLs98} for 1.125 +more details on object-oriented verification and record subtyping in HOL. 1.126 + 1.127 + 1.128 +\subsection{Basic concepts} 1.129 + 1.130 +Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the 1.131 +level of terms and types. The notation is as follows: 1.132 + 1.133 +\begin{center} 1.134 +\begin{tabular}{l|l|l} 1.135 + & record terms & record types \\ \hline 1.136 + fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\ 1.137 + schematic & $\record{x = a\fs y = b\fs \more = m}$ & 1.138 + $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\ 1.139 +\end{tabular} 1.140 +\end{center} 1.141 + 1.142 +\noindent The ASCII representation of $\record{x = a}$ is \texttt{(| x = a |)}. 1.143 + 1.144 +A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field 1.145 +$y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$, 1.146 +assuming that $a \ty A$ and $b \ty B$. 1.147 1.148 -FIXME proof tools (simp, cases/induct; no split!?); 1.149 +A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields 1.150 +$x$ and $y$ as before, but also possibly further fields as indicated by the 1.151 +``$\more$'' notation (which is actually part of the syntax). The improper 1.152 +field ``$\more$'' of a record scheme is called the \emph{more part}. 1.153 +Logically it is just a free variable, which is occasionally referred to as 1.154 +\emph{row variable} in the literature. The more part of a record scheme may 1.155 +be instantiated by zero or more further components. For example, the above 1.156 +scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = 1.157 + m'}$, where $m'$ refers to a different more part. Fixed records are special 1.158 +instances of record schemes, where ``$\more$'' is properly terminated by the 1.159 +$() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an 1.160 +abbreviation for $\record{x = a\fs y = b\fs \more = ()}$. 1.161 + 1.162 +\medskip 1.163 1.164 -FIXME mixfix syntax; 1.165 +Two key observations make extensible records in a simply typed language like 1.166 +HOL feasible: 1.167 +\begin{enumerate} 1.168 +\item the more part is internalized, as a free term or type variable, 1.169 +\item field names are externalized, they cannot be accessed within the logic 1.170 + as first-class values. 1.171 +\end{enumerate} 1.172 + 1.173 +\medskip 1.174 + 1.175 +In Isabelle/HOL record types have to be defined explicitly, fixing their field 1.176 +names and types, and their (optional) parent record (see 1.177 +{\S}\ref{sec:hol-record-def}). Afterwards, records may be formed using above 1.178 +syntax, while obeying the canonical order of fields as given by their 1.179 +declaration. The record package provides several standard operations like 1.180 +selectors and updates (see {\S}\ref{sec:hol-record-ops}). The common setup 1.181 +for various generic proof tools enable succinct reasoning patterns (see 1.182 +{\S}\ref{sec:hol-record-thms}). See also the Isabelle/HOL tutorial 1.183 +\cite{isabelle-hol-book} for further instructions on using records in 1.184 +practice. 1.185 + 1.186 + 1.187 +\subsection{Record specifications}\label{sec:hol-record-def} 1.188 1.189 \indexisarcmdof{HOL}{record} 1.190 \begin{matharray}{rcl} 1.191 @@ -162,10 +245,135 @@ 1.192 \item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] 1.193 defines extensible record type $(\vec\alpha)t$, derived from the optional 1.194 parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$. 1.195 - See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on 1.196 - simply-typed extensible records. 1.197 + 1.198 + The type variables of $\tau$ and $\vec\sigma$ need to be covered by the 1.199 + (distinct) parameters $\vec\alpha$. Type constructor $t$ has to be new, 1.200 + while $\tau$ needs to specify an instance of an existing record type. At 1.201 + least one new field $\vec c$ has to be specified. Basically, field names 1.202 + need to belong to a unique record. This is not a real restriction in 1.203 + practice, since fields are qualified by the record name internally. 1.204 + 1.205 + The parent record specification $\tau$ is optional; if omitted $t$ becomes a 1.206 + root record. The hierarchy of all records declared within a theory context 1.207 + forms a forest structure, i.e.\ a set of trees starting with a root record 1.208 + each. There is no way to merge multiple parent records! 1.209 + 1.210 + For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the 1.211 + fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is 1.212 + $(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c 1.213 + \ty \vec\sigma\fs \more \ty \zeta}$. 1.214 + 1.215 \end{descr} 1.216 1.217 +\subsection{Record operations}\label{sec:hol-record-ops} 1.218 + 1.219 +Any record definition of the form presented above produces certain standard 1.220 +operations. Selectors and updates are provided for any field, including the 1.221 +improper one ``$more$''. There are also cumulative record constructor 1.222 +functions. To simplify the presentation below, we assume for now that 1.223 +$(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$. 1.224 + 1.225 +\medskip \textbf{Selectors} and \textbf{updates} are available for any field 1.226 +(including ``$more$''): 1.227 +\begin{matharray}{lll} 1.228 + c@i & \ty & \record{\vec c \ty \vec \sigma, \more \ty \zeta} \To \sigma@i \\ 1.229 + c@i_update & \ty & \sigma@i \To \record{\vec c \ty \vec\sigma, \more \ty \zeta} \To 1.230 + \record{\vec c \ty \vec\sigma, \more \ty \zeta} 1.231 +\end{matharray} 1.232 + 1.233 +There is special syntax for application of updates: $r \, \record{x \asn a}$ 1.234 +abbreviates term $x_update \, a \, r$. Further notation for repeated updates 1.235 +is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z 1.236 + \asn c}$ may be written $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. 1.237 +Note that because of postfix notation the order of fields shown here is 1.238 +reverse than in the actual term. Since repeated updates are just function 1.239 +applications, fields may be freely permuted in $\record{x \asn a\fs y \asn 1.240 + b\fs z \asn c}$, as far as logical equality is concerned. Thus 1.241 +commutativity of updates can be proven within the logic for any two fields, 1.242 +but not as a general theorem: fields are not first-class values. 1.243 + 1.244 +\medskip The \textbf{make} operation provides a cumulative record constructor 1.245 +functions: 1.246 +\begin{matharray}{lll} 1.247 + t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\ 1.248 +\end{matharray} 1.249 + 1.250 +\medskip We now reconsider the case of non-root records, which are derived of 1.251 +some parent. In general, the latter may depend on another parent as well, 1.252 +resulting in a list of \emph{ancestor records}. Appending the lists of fields 1.253 +of all ancestors results in a certain field prefix. The record package 1.254 +automatically takes care of this by lifting operations over this context of 1.255 +ancestor fields. Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec 1.256 +b \ty \vec\rho$, the above record operations will get the following types: 1.257 +\begin{matharray}{lll} 1.258 + c@i & \ty & \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty 1.259 + \zeta} \To \sigma@i \\ 1.260 + c@i_update & \ty & \sigma@i \To 1.261 + \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To 1.262 + \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\ 1.263 + t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To 1.264 + \record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\ 1.265 +\end{matharray} 1.266 +\noindent 1.267 + 1.268 +\medskip Some further operations address the extension aspect of a derived 1.269 +record scheme specifically: $fields$ produces a record fragment consisting of 1.270 +exactly the new fields introduced here (the result may serve as a more part 1.271 +elsewhere); $extend$ takes a fixed record and adds a given more part; 1.272 +$truncate$ restricts a record scheme to a fixed record. 1.273 + 1.274 +\begin{matharray}{lll} 1.275 + t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\ 1.276 + t{\dtt}extend & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \To 1.277 + \zeta \To \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\ 1.278 + t{\dtt}truncate & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To 1.279 + \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\ 1.280 +\end{matharray} 1.281 + 1.282 +\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ are actually coincide for root records. 1.283 + 1.284 + 1.285 +\subsection{Derived rules and proof tools}\label{sec:hol-record-thms} 1.286 + 1.287 +The record package proves several results internally, declaring these facts to 1.288 +appropriate proof tools. This enables users to reason about record structures 1.289 +quite comfortably. Assume that $t$ is a record type as specified above. 1.290 + 1.291 +\begin{enumerate} 1.292 + 1.293 +\item Standard conversions for selectors or updates applied to record 1.294 + constructor terms are made part of the default Simplifier context; thus 1.295 + proofs by reduction of basic operations merely require the $simp$ method 1.296 + without further arguments. These rules are available as $t{\dtt}simps$. 1.297 + 1.298 +\item Selectors applied to updated records are automatically reduced by an 1.299 + internal simplification procedure, which is also part of the default 1.300 + Simplifier context. 1.301 + 1.302 +\item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x' 1.303 + \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$ 1.304 + rules. These rules are available as $t{\dtt}iffs$. 1.305 + 1.306 +\item The introduction rule for record equality analogous to $x~r = x~r' \Imp 1.307 + y~r = y~r' \Imp \dots \Imp r = r'$ is declared to the Simplifier, and as the 1.308 + basic rule context as ``$intro?$''. The rule is called $t{\dtt}equality$. 1.309 + 1.310 +\item Representations of arbitrary record expressions as canonical constructor 1.311 + terms are provided both in $cases$ and $induct$ format (cf.\ the generic 1.312 + proof methods of the same name, \S\ref{sec:cases-induct}). Several 1.313 + variations are available, for fixed records, record schemes, more parts etc. 1.314 + 1.315 + The generic proof methods are sufficiently smart to pick the most sensible 1.316 + rule according to the type of the indicated record expression: users just 1.317 + need to apply something like ``$(cases r)$'' to a certain proof problem. 1.318 + 1.319 +\item The derived record operations $t{\dtt}make$, $t{\dtt}fields$, 1.320 + $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but 1.321 + usually need to be expanded by hand, using the collective fact 1.322 + $t{\dtt}defs$. 1.323 + 1.324 +\end{enumerate} 1.325 + 1.326 1.327 \subsection{Datatypes}\label{sec:hol-datatype} 1.328 1.329 @@ -202,12 +410,12 @@ 1.330 to the constructors involved, while parameters are named after the types (see 1.331 also \S\ref{sec:cases-induct}). 1.332 1.333 -See \cite{isabelle-HOL} for more details on datatypes. Note that the theory 1.334 -syntax above has been slightly simplified over the old version, usually 1.335 -requiring more quotes and less parentheses. Apart from proper proof methods 1.336 -for case-analysis and induction, there are also emulations of ML tactics 1.337 +See \cite{isabelle-HOL} for more details on datatypes, but beware of the 1.338 +old-style theory syntax being used there! Apart from proper proof methods for 1.339 +case-analysis and induction, there are also emulations of ML tactics 1.340 \texttt{case_tac} and \texttt{induct_tac} available, see 1.341 -\S\ref{sec:induct_tac}. 1.342 +\S\ref{sec:induct_tac}; these admit to refer directly to the internal 1.343 +structure of subgoals (including internally bound parameters). 1.344 1.345 1.346 \subsection{Recursive functions}\label{sec:recursion} 1.347 @@ -253,25 +461,25 @@ 1.348 1.349 \begin{descr} 1.350 \item [$\isarkeyword{primrec}$] defines primitive recursive functions over 1.351 - datatypes, see also \cite{isabelle-HOL}. 1.352 + datatypes, see also \cite{isabelle-HOL} FIXME. 1.353 \item [$\isarkeyword{recdef}$] defines general well-founded recursive 1.354 - functions (using the TFL package), see also \cite{isabelle-HOL}. The 1.355 + functions (using the TFL package), see also \cite{isabelle-HOL} FIXME. The 1.356 $(permissive)$ option tells TFL to recover from failed proof attempts, 1.357 returning unfinished results. The $recdef_simp$, $recdef_cong$, and 1.358 $recdef_wf$ hints refer to auxiliary rules to be used in the internal 1.359 - automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\ 1.360 + automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\ 1.361 \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier 1.362 - (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ 1.363 + (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ 1.364 \S\ref{sec:classical}). 1.365 \item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover 1.366 termination condition number $i$ (default $1$) as generated by a 1.367 $\isarkeyword{recdef}$ definition of constant $c$. 1.368 - 1.369 + 1.370 Note that in most cases, $\isarkeyword{recdef}$ is able to finish its 1.371 internal proofs without manual intervention. 1.372 \end{descr} 1.373 1.374 -Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 1.375 +Both kinds of recursive definitions accommodate reasoning by induction (cf.\ 1.376 \S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of 1.377 the function definition) refers to a specific induction rule, with parameters 1.378 named according to the user-specified equations. Case names of 1.379 @@ -342,8 +550,8 @@ 1.380 automated monotonicity proof of $\isarkeyword{inductive}$. 1.381 \end{descr} 1.382 1.383 -See \cite{isabelle-HOL} for further information on inductive definitions in 1.384 -HOL. 1.385 +See \cite{isabelle-HOL} FIXME for further information on inductive definitions 1.386 +in HOL. 1.387 1.388 1.389 \subsection{Arithmetic proof support} 1.390 @@ -402,7 +610,7 @@ 1.391 ; 1.392 indcases (prop +) 1.393 ; 1.394 - inductivecases thmdecl? (prop +) 1.395 + inductivecases (thmdecl? (prop +) + 'and') 1.396 ; 1.397 1.398 rule: ('rule' ':' thmref) 1.399 @@ -417,11 +625,11 @@ 1.400 both goal addressing and dynamic instantiation. Note that named rule cases 1.401 are \emph{not} provided as would be by the proper $induct$ and $cases$ proof 1.402 methods (see \S\ref{sec:cases-induct}). 1.403 - 1.404 + 1.405 \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface 1.406 to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted 1.407 forward manner. 1.408 - 1.409 + 1.410 While $ind_cases$ is a proof method to apply the result immediately as 1.411 elimination rules, $\isarkeyword{inductive_cases}$ provides case split 1.412 theorems at the theory level for later use, 1.413 @@ -471,14 +679,12 @@ 1.414 dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs 1.415 \end{rail} 1.416 1.417 -Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 1.418 +Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 1.419 \S\ref{sec:hol-datatype}). Mutual recursive is supported, but no nesting nor 1.420 arbitrary branching. Domain constructors may be strict (default) or lazy, the 1.421 -latter admits to introduce infinitary objects in the typical LCF manner (lazy 1.422 -lists etc.). 1.423 - 1.424 -See also \cite{MuellerNvOS99} for further information HOLCF domains in 1.425 -general. 1.426 +latter admits to introduce infinitary objects in the typical LCF manner (e.g.\ 1.427 +lazy lists). See also \cite{MuellerNvOS99} for a general discussion of HOLCF 1.428 +domains. 1.429 1.430 1.431 \section{ZF} 1.432 @@ -492,7 +698,7 @@ 1.433 FIXME 1.434 1.435 1.436 -%%% Local Variables: 1.437 +%%% Local Variables: 1.438 %%% mode: latex 1.439 %%% TeX-master: "isar-ref" 1.440 -%%% End: 1.441 +%%% End: