Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
improved README -- Isabelle symbols and fonts;
authorwenzelm
Mon, 24 Jan 2011 21:30:33 +0100
changeset 41876ed4d793f0c26
parent 41875 0040e0ea02e7
child 41877 8ff597b3dd80
child 41878 5490dc4d999d
improved README -- Isabelle symbols and fonts;
src/Tools/jEdit/dist-template/README.html file | annotate | diff | comparison | revisions 
     1.1 --- a/src/Tools/jEdit/dist-template/README.html	Mon Jan 24 15:39:42 2011 +0100
     1.2 +++ b/src/Tools/jEdit/dist-template/README.html	Mon Jan 24 21:30:33 2011 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -<?xml version="1.0" encoding="ISO-8859-1" ?>
     1.5 +<?xml version="1.0" encoding="UTF-8" ?>
     1.6  <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
     1.7  <html xmlns="http://www.w3.org/1999/xhtml">
     1.8  
     1.9 @@ -9,7 +9,7 @@
    1.10  
    1.11  <body>
    1.12  
    1.13 -<h2>Notes on the Isabelle/jEdit Prover IDE</h2>
    1.14 +<h2>The Isabelle/jEdit Prover IDE</h2>
    1.15  
    1.16  <ul>
    1.17  
    1.18 @@ -34,6 +34,70 @@
    1.19  
    1.20  </ul>
    1.21  
    1.22 +
    1.23 +<h2>Isabelle symbols and fonts</h2>
    1.24 +
    1.25 +<ul>
    1.26 +
    1.27 +  <li>Isabelle supports infinitely many symbols:<br/>
    1.28 +    &alpha;, &beta;, &gamma;, &hellip;<br/>
    1.29 +    &forall;, &exist;, &or;, &and;, &#10230;, &#10231;, &hellip;<br/>
    1.30 +    &le;, &ge;, &#8851;, &#8852;, &hellip;<br/>
    1.31 +    &#8501;, &#9651;, &#8711;, &hellip;<br/>
    1.32 +    <tt>\&lt;foo&gt;</tt>, <tt>\&lt;bar&gt;</tt>, <tt>\&lt;baz&gt;</tt>, &hellip;<br/>
    1.33 +  </li>
    1.34 +
    1.35 +  <li>A default mapping relates some Isabelle symbols to Unicode points
    1.36 +    (see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>).
    1.37 +  </li>
    1.38 +
    1.39 +  <li>The <em>IsabelleText</em> font ensures that Unicode points are actually
    1.40 +    seen on the screen (or printer).
    1.41 +  </li>
    1.42 +
    1.43 +  <li>Input methods:
    1.44 +    <ul>
    1.45 +      <li>copy/paste from decoded source files</li>
    1.46 +      <li>copy/paste from prover output</li>
    1.47 +      <li>completion provided by Isabelle plugin, e.g.<br/>
    1.48 +
    1.49 +      <table border="1">
    1.50 +      <tr><th><b>name</b></th>    <th><b>abbreviation</b></th>  <th><b>symbol</b></th></tr>
    1.51 +
    1.52 +      <tr><td>lambda</td>         <td></td>                     <td>&lambda;</td></tr>
    1.53 +      <tr><td>Rightarrow</td>     <td><tt>=&gt;</tt></td>       <td>&#8658;</td></tr>
    1.54 +      <tr><td>Longrightarrow</td> <td><tt>==&gt;</tt></td>      <td>&#10233;</td></tr>
    1.55 +
    1.56 +      <tr><td>And</td>            <td><tt>!!</tt></td>          <td>&#8896;</td></tr>
    1.57 +      <tr><td>equiv</td>          <td><tt>==</tt></td>          <td>&equiv;</td></tr>
    1.58 +
    1.59 +      <tr><td>forall</td>         <td><tt>!</tt></td>           <td>&forall;</td></tr>
    1.60 +      <tr><td>exists</td>         <td><tt>?</tt></td>           <td>&exist;</td></tr>
    1.61 +      <tr><td>longrightarrow</td> <td><tt>--&gt;</tt></td>      <td>&#10230;</td></tr>
    1.62 +      <tr><td>and</td>            <td><tt>/\</tt></td>          <td>&and;</td></tr>
    1.63 +      <tr><td>or</td>             <td><tt>\/</tt></td>          <td>&or;</td></tr>
    1.64 +      <tr><td>not</td>            <td><tt>~ </tt></td>          <td>&not;</td></tr>
    1.65 +      <tr><td>noteq</td>          <td><tt>~=</tt></td>          <td>&ne;</td></tr>
    1.66 +      <tr><td>in</td>             <td><tt>:</tt></td>           <td>&isin;</td></tr>
    1.67 +      <tr><td>notin</td>          <td><tt>~:</tt></td>          <td>&notin;</td></tr>
    1.68 +    </table>
    1.69 +    </li>
    1.70 +  </ul>
    1.71 +  </li>
    1.72 +
    1.73 +  <li><b>NOTE:</b> The above abbreviations refer to the input method.
    1.74 +    The logical notation provides ASCII alternatives that often
    1.75 +    coincide, but deviate occasionally.
    1.76 +  </li>
    1.77 +
    1.78 +  <li><b>NOTE:</b> Generic jEdit abbreviations or plugins perform similar
    1.79 +    source replacement operations; this works for Isabelle as long
    1.80 +    as the Unicode sequences coincide with the symbol mapping.
    1.81 +  </li>
    1.82 +
    1.83 +</ul>
    1.84 +
    1.85 +
    1.86  <h2>Limitations and workrounds (January 2011)</h2>
    1.87  
    1.88  <ul>
wneuper/isa