diff -r 7c3726a3dbec -r c039b8ede204 doc-src/IsarRef/logics.tex
--- 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