tuned;
authorwenzelm
Mon Mar 04 22:31:21 2002 +0100 (2002-03-04)
changeset 13016c039b8ede204
parent 13015 7c3726a3dbec
child 13017 c28df0f7ebdb
tuned;
README.html
doc-src/IsarRef/logics.tex
doc-src/IsarRef/pure.tex
     1.1 --- a/README.html	Mon Mar 04 19:08:15 2002 +0100
     1.2 +++ b/README.html	Mon Mar 04 22:31:21 2002 +0100
     1.3 @@ -29,9 +29,9 @@
     1.4  Furthermore, Isabelle needs the following software, which is not part
     1.5  of the distribution:
     1.6  <ul>
     1.7 -<li> A full Standard ML Compiler (e.g. Poly/ML).
     1.8 -<li> The GNU bash shell (version 1.x or 2.x).
     1.9 -<li> Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
    1.10 +<li>A full Standard ML Compiler (e.g. Poly/ML).
    1.11 +<li>The GNU bash shell (version 1.x or 2.x).
    1.12 +<li>Perl 5.x - the Pathologically Eclectic Rubbish Lister (Perl 4.x
    1.13  is <em>not</em> sufficient).
    1.14  </ul>
    1.15  
    1.16 @@ -40,8 +40,8 @@
    1.17  The following ML system and platform combinations are known to work
    1.18  very well:
    1.19  <ul>
    1.20 -<li> Poly/ML 4.x and 3.x on Linux/x86, Solaris/Sparc, and PowerPC platforms.
    1.21 -<li> SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
    1.22 +<li>Poly/ML 4.x and 3.x on Linux/x86, Solaris/Sparc, and PowerPC platforms.
    1.23 +<li>SML/NJ 110.x on any Unix platform (Linux, Suns, SGI etc.).
    1.24  </ul>
    1.25  
    1.26  <p> <a href="http://www.polyml.org/">Poly/ML</a>, previously a
    1.27 @@ -101,10 +101,10 @@
    1.28  
    1.29  <ul>
    1.30  
    1.31 -<li> <a
    1.32 +<li><a
    1.33  href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">http://www.cl.cam.ac.uk/Research/HVG/Isabelle/</a>
    1.34  
    1.35 -<li> <a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
    1.36 +<li><a href="http://isabelle.in.tum.de">http://isabelle.in.tum.de</a>
    1.37  
    1.38  </ul>
    1.39  
     2.1 --- a/doc-src/IsarRef/logics.tex	Mon Mar 04 19:08:15 2002 +0100
     2.2 +++ b/doc-src/IsarRef/logics.tex	Mon Mar 04 22:31:21 2002 +0100
     2.3 @@ -34,9 +34,6 @@
     2.4  declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
     2.5  Reasoner \S\ref{sec:classical}).
     2.6  
     2.7 -\railalias{ruleformat}{rule\_format}
     2.8 -\railterm{ruleformat}
     2.9 -
    2.10  \begin{rail}
    2.11    'judgment' constdecl
    2.12    ;
    2.13 @@ -96,7 +93,12 @@
    2.14  \begin{rail}
    2.15    'typedecl' typespec infix?
    2.16    ;
    2.17 -  'typedef' parname? typespec infix? '=' term
    2.18 +  'typedef' parname? abstype '=' repset
    2.19 +  ;
    2.20 +
    2.21 +  abstype: typespec infix?
    2.22 +  ;
    2.23 +  repset: term ('morphisms' name name)?
    2.24    ;
    2.25  \end{rail}
    2.26  
    2.27 @@ -113,17 +115,22 @@
    2.28    bijection between the representing set $A$ and the new type $t$.
    2.29    
    2.30    Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term
    2.31 -  constant) of the same name.  The injection from type to set is called
    2.32 -  $Rep_t$, its inverse $Abs_t$.  Theorems $Rep_t$, $Rep_inverse$, and
    2.33 -  $Abs_inverse$ provide the most basic characterization as a corresponding
    2.34 -  injection/surjection pair (in both directions).  Rules $Rep_t_inject$ and
    2.35 -  $Abs_t_inject$ provide a slightly more comfortable view on the injectivity
    2.36 -  part; likewise do $Rep_t_cases$, $Rep_t_induct$, and $Abs_t_cases$,
    2.37 -  $Abs_t_induct$ for surjectivity.  The latter rules are already declare as
    2.38 -  type or set rules for the generic $cases$ and $induct$ methods.
    2.39 +  constant) of the same name (an alternative base name may be given in
    2.40 +  parentheses).  The injection from type to set is called $Rep_t$, its inverse
    2.41 +  $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$
    2.42 +  declaration).
    2.43 +  
    2.44 +  Theorems $Rep_t$, $Rep_inverse$, and $Abs_inverse$ provide the most basic
    2.45 +  characterization as a corresponding injection/surjection pair (in both
    2.46 +  directions).  Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly
    2.47 +  more comfortable view on the injectivity part, suitable for automated proof
    2.48 +  tools (e.g.\ in $simp$ or $iff$ declarations).  Rules $Rep_t_cases$,
    2.49 +  $Rep_t_induct$, and $Abs_t_cases$, $Abs_t_induct$ provide alternative views
    2.50 +  on surjectivity; these are already declared as type or set rules for the
    2.51 +  generic $cases$ and $induct$ methods.
    2.52  \end{descr}
    2.53  
    2.54 -Raw type declarations are rarely useful in practice.  The main application is
    2.55 +Raw type declarations are rarely used in practice; the main application is
    2.56  with experimental (or even axiomatic!) theory fragments.  Instead of primitive
    2.57  HOL type definitions, user-level theories usually refer to higher-level
    2.58  packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or
     3.1 --- a/doc-src/IsarRef/pure.tex	Mon Mar 04 19:08:15 2002 +0100
     3.2 +++ b/doc-src/IsarRef/pure.tex	Mon Mar 04 22:31:21 2002 +0100
     3.3 @@ -754,22 +754,22 @@
     3.4  (\S\ref{sec:tactic-commands}).\footnote{The $induct$ method covered in
     3.5    \S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.}
     3.6  
     3.7 -Claims at the theory level may be either in ``short'' or ``long'' form.  A
     3.8 -short goal merely consists of several simultaneous propositions (often just
     3.9 -one).  A long goal includes an explicit context specification for the
    3.10 -subsequent conclusions, involving local parameters; here the role of each part
    3.11 -of the statement is explicitly marked by separate keywords (see also
    3.12 +Claims at the theory level may be either in short or long form.  A short goal
    3.13 +merely consists of several simultaneous propositions (often just one).  A long
    3.14 +goal includes an explicit context specification for the subsequent
    3.15 +conclusions, involving local parameters; here the role of each part of the
    3.16 +statement is explicitly marked by separate keywords (see also
    3.17  \S\ref{sec:locale}).
    3.18  
    3.19  \begin{rail}
    3.20 -  ('lemma' | 'theorem' | 'corollary') locale? (shortgoal | longgoal)
    3.21 +  ('lemma' | 'theorem' | 'corollary') locale? (goal | longgoal)
    3.22    ;
    3.23 -  ('have' | 'show' | 'hence' | 'thus') shortgoal
    3.24 +  ('have' | 'show' | 'hence' | 'thus') goal
    3.25    ;
    3.26    
    3.27 -  shortgoal: (props + 'and')
    3.28 +  goal: (props + 'and')
    3.29    ;
    3.30 -  longgoal: thmdecl? (contextelem *) 'shows' shortgoal
    3.31 +  longgoal: thmdecl? (contextelem *) 'shows' goal
    3.32    ;
    3.33  \end{rail}
    3.34