src/HOL/Library/README.html
changeset 10282 b7d96e94796f
parent 10253 73b46b18c348
child 10334 e5e6070fcef5
equal deleted inserted replaced
10281:9554ce1c2e54 10282:b7d96e94796f
    20 clashes with existing developments.
    20 clashes with existing developments.
    21 
    21 
    22 <dl>
    22 <dl>
    23 
    23 
    24 <dt><strong>Files</strong>
    24 <dt><strong>Files</strong>
       
    25 
    25 <dd>Avoid unnecessary scattering of theories over several files.  Use
    26 <dd>Avoid unnecessary scattering of theories over several files.  Use
    26 new-style theories only, as old ones tend to clutter the file space
    27 new-style theories only, as old ones tend to clutter the file space
    27 with separate <tt>.thy</tt> and <tt>.ML</tt> files.
    28 with separate <tt>.thy</tt> and <tt>.ML</tt> files.
    28 
    29 
    29 <dt><strong>Examples</strong>
    30 <dt><strong>Examples</strong>
    30 
    31 
    31 <dd>Theories should be as ``generic'' as is sensible.  Unused (or
    32 <dd>Theories should be as ``generic'' as is sensible.  Unused (or
    32 rather unusable?) standalone theories should be avoided; common
    33 rather unusable?) theories should be avoided; common applications
    33 applications should actually refer to the present theory.  Small
    34 should actually refer to the present theory.  Small example uses may
    34 example uses may be included as well, but should be put in a separate
    35 be included in the library as well, but should be put in a separate
    35 theory, such as <tt>Foobar</tt> accompanied by
    36 theory, such as <tt>Foobar</tt> accompanied by
    36 <tt>Foobar_Examples</tt>.
    37 <tt>Foobar_Examples</tt>.
    37 
    38 
    38 <dt><strong>Theory names</strong>
    39 <dt><strong>Theory names</strong>
       
    40 
    39 <dd>The theory loader name space is <em>flat</em>, so use sufficiently
    41 <dd>The theory loader name space is <em>flat</em>, so use sufficiently
    40 long and descriptive names to reduce the danger of clashes with the
    42 long and descriptive names to reduce the danger of clashes with the
    41 user's own theories.  The convention for theory names is as follows:
    43 user's own theories.  The convention for theory names is as follows:
    42 <tt>Foobar_Doobar</tt> (this looks best in LaTeX output).
    44 <tt>Foobar_Doobar</tt> (this looks best in LaTeX output).
    43 
    45 
    44 <dt><strong>Names of logical items</strong>
    46 <dt><strong>Names of logical items</strong>
       
    47 
    45 <dd>There are separate hierarchically structured name spaces for
    48 <dd>There are separate hierarchically structured name spaces for
    46 types, constants, theorems etc.  Nevertheless, some care should be
    49 types, constants, theorems etc.  Nevertheless, some care should be
    47 taken, as the name spaces are always ``open''.  Use adequate names;
    50 taken, as the name spaces are always ``open''.  Use adequate names;
    48 avoid unreadable abbreviations.  The general naming convention is to
    51 avoid unreadable abbreviations.  The general naming convention is to
    49 separate word constituents by underscores, as in <tt>foo_bar</tt> or
    52 separate word constituents by underscores, as in <tt>foo_bar</tt> or
    54 Note that syntax is <em>global</em>; qualified names loose syntax on
    57 Note that syntax is <em>global</em>; qualified names loose syntax on
    55 output.  Do not use ``exotic'' symbols for syntax (such as
    58 output.  Do not use ``exotic'' symbols for syntax (such as
    56 <tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    59 <tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    57 
    60 
    58 <dt><strong>Global context declarations</strong>
    61 <dt><strong>Global context declarations</strong>
       
    62 
    59 <dd>Only items introduced in the present theory should be declared
    63 <dd>Only items introduced in the present theory should be declared
    60 globally (e.g. as Simplifier rules).  Note that adding / deleting
    64 globally (e.g. as Simplifier rules).  Note that adding and deleting
    61 rules stemming from parent theories may result in strange behavior
    65 rules from parent theories may result in strange behavior later,
    62 later, depending on the user's arrangement of import lists.
    66 depending on the user's arrangement of import lists.
    63 
    67 
    64 <dt><strong>Mathematical symbols</strong>
    68 <dt><strong>Mathematical symbols</strong>
    65 <dd>Non-ASCII symbols should be used with some care. In particular,
    69 
    66 avoid unreadable arrows: <tt>==&gt;</tt> should be preferred over
    70 <dd>Non-ASCII symbols should be used as appropriate, with some
    67 <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool unsymbolize</tt> to
    71 care. In particular, avoid unreadable arrows: <tt>==&gt;</tt> should
    68 clean up the sources.
    72 be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool
       
    73 unsymbolize</tt> to clean up the sources.
    69 
    74 
    70 <p>
    75 <p>
    71 
    76 
    72 The following ASCII symbols of HOL should be generally avoided:
    77 The following ASCII symbols of HOL should be generally avoided:
    73 <tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
    78 <tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
    74 use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\&lt;forall&gt;</tt>),
    79 use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\&lt;forall&gt;</tt>),
    75 <tt>EX</tt> (or <tt>\&lt;exists&gt;</tt>), <tt>EX!</tt> (or
    80 <tt>EX</tt> (or <tt>\&lt;exists&gt;</tt>), <tt>EX!</tt> (or
    76 <tt>\&lt;exists;&gt!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
    81 <tt>\&lt;exists&gt;!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
    77 Note that bracket notation <tt>[|&nbsp;|]</tt> looks bad in LaTeX
    82 Note that bracket notation <tt>[|&nbsp;|]</tt> looks bad in LaTeX
    78 output.
    83 output.
    79 
    84 
    80 <p>
    85 <p>
    81 
    86 
    82 Some additional mathematical symbols are quite suitable for both
    87 Some additional mathematical symbols are quite suitable for both
    83 readable sources and output document:
    88 readable sources and the output document:
    84 <tt>\&lt;Inter&gt;</tt>,
    89 <tt>\&lt;Inter&gt;</tt>,
    85 <tt>\&lt;Union&gt;</tt>,
    90 <tt>\&lt;Union&gt;</tt>,
    86 <tt>\&lt;and&gt;</tt>,
    91 <tt>\&lt;and&gt;</tt>,
    87 <tt>\&lt;in&gt;</tt>,
    92 <tt>\&lt;in&gt;</tt>,
    88 <tt>\&lt;inter&gt;</tt>,
    93 <tt>\&lt;inter&gt;</tt>,