tuned;
authorwenzelm
Mon, 04 Mar 2002 22:31:21 +0100 (2002-03-04)
changeset 13016 c039b8ede204
parent 13015 7c3726a3dbec
child 13017 c28df0f7ebdb
tuned;
README.html
doc-src/IsarRef/logics.tex
doc-src/IsarRef/pure.tex
--- 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}