--- a/README.html Mon Mar 04 19:08:15 2002 +0100
+++ b/README.html Mon Mar 04 22:31:21 2002 +0100
@@ -29,9 +29,9 @@
Furthermore, Isabelle needs the following software, which is not part
of the distribution:
<ul>
-<li> A full Standard ML Compiler (e.g. Poly/ML).
-<li> The GNU bash shell (version 1.x or 2.x).
-<li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
+<li>A full Standard ML Compiler (e.g. Poly/ML).
+<li>The GNU bash shell (version 1.x or 2.x).
+<li>Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
is <em>not</em> sufficient).
</ul>
@@ -40,8 +40,8 @@
The following ML system and platform combinations are known to work
very well:
<ul>
-<li> Poly/ML 4.x and 3.x on Linux/x86, Solaris/Sparc, and PowerPC platforms.
-<li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
+<li>Poly/ML 4.x and 3.x on Linux/x86, Solaris/Sparc, and PowerPC platforms.
+<li>SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
</ul>
<p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a
@@ -101,10 +101,10 @@
<ul>
-<li> <a
+<li><a
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a>
-<li> <a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
+<li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
</ul>
--- a/doc-src/IsarRef/logics.tex Mon Mar 04 19:08:15 2002 +0100
+++ b/doc-src/IsarRef/logics.tex Mon Mar 04 22:31:21 2002 +0100
@@ -34,9 +34,6 @@
declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
Reasoner \S\ref{sec:classical}).
-\railalias{ruleformat}{rule\_format}
-\railterm{ruleformat}
-
\begin{rail}
'judgment' constdecl
;
@@ -96,7 +93,12 @@
\begin{rail}
'typedecl' typespec infix?
;
- 'typedef' parname? typespec infix? '=' term
+ 'typedef' parname? abstype '=' repset
+ ;
+
+ abstype: typespec infix?
+ ;
+ repset: term ('morphisms' name name)?
;
\end{rail}
@@ -113,17 +115,22 @@
bijection between the representing set $A$ and the new type $t$.
Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term
- constant) of the same name. The injection from type to set is called
- $Rep_t$, its inverse $Abs_t$. Theorems $Rep_t$, $Rep_inverse$, and
- $Abs_inverse$ provide the most basic characterization as a corresponding
- injection/surjection pair (in both directions). Rules $Rep_t_inject$ and
- $Abs_t_inject$ provide a slightly more comfortable view on the injectivity
- part; likewise do $Rep_t_cases$, $Rep_t_induct$, and $Abs_t_cases$,
- $Abs_t_induct$ for surjectivity. The latter rules are already declare as
- type or set rules for the generic $cases$ and $induct$ methods.
+ constant) of the same name (an alternative base name may be given in
+ parentheses). The injection from type to set is called $Rep_t$, its inverse
+ $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$
+ declaration).
+
+ Theorems $Rep_t$, $Rep_inverse$, and $Abs_inverse$ provide the most basic
+ characterization as a corresponding injection/surjection pair (in both
+ directions). Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly
+ more comfortable view on the injectivity part, suitable for automated proof
+ tools (e.g.\ in $simp$ or $iff$ declarations). Rules $Rep_t_cases$,
+ $Rep_t_induct$, and $Abs_t_cases$, $Abs_t_induct$ provide alternative views
+ on surjectivity; these are already declared as type or set rules for the
+ generic $cases$ and $induct$ methods.
\end{descr}
-Raw type declarations are rarely useful in practice. The main application is
+Raw type declarations are rarely used in practice; the main application is
with experimental (or even axiomatic!) theory fragments. Instead of primitive
HOL type definitions, user-level theories usually refer to higher-level
packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or
--- a/doc-src/IsarRef/pure.tex Mon Mar 04 19:08:15 2002 +0100
+++ b/doc-src/IsarRef/pure.tex Mon Mar 04 22:31:21 2002 +0100
@@ -754,22 +754,22 @@
(\S\ref{sec:tactic-commands}).\footnote{The $induct$ method covered in
\S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.}
-Claims at the theory level may be either in ``short'' or ``long'' form. A
-short goal merely consists of several simultaneous propositions (often just
-one). A long goal includes an explicit context specification for the
-subsequent conclusions, involving local parameters; here the role of each part
-of the statement is explicitly marked by separate keywords (see also
+Claims at the theory level may be either in short or long form. A short goal
+merely consists of several simultaneous propositions (often just one). A long
+goal includes an explicit context specification for the subsequent
+conclusions, involving local parameters; here the role of each part of the
+statement is explicitly marked by separate keywords (see also
\S\ref{sec:locale}).
\begin{rail}
- ('lemma' | 'theorem' | 'corollary') locale? (shortgoal | longgoal)
+ ('lemma' | 'theorem' | 'corollary') locale? (goal | longgoal)
;
- ('have' | 'show' | 'hence' | 'thus') shortgoal
+ ('have' | 'show' | 'hence' | 'thus') goal
;
- shortgoal: (props + 'and')
+ goal: (props + 'and')
;
- longgoal: thmdecl? (contextelem *) 'shows' shortgoal
+ longgoal: thmdecl? (contextelem *) 'shows' goal
;
\end{rail}