Poly/ML, previously a @@ -101,10 +101,10 @@
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 diff -r 7c3726a3dbec -r c039b8ede204 doc-src/IsarRef/pure.tex --- 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}