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