src/HOL/Library/README.html
changeset 28504 7ad7d7d6df47
parent 26406 be5b78d95801
child 31975 366ad09d39ef
equal deleted inserted replaced
28503:a30b7169fdd1 28504:7ad7d7d6df47
    72 
    72 
    73 <dt><strong>Mathematical symbols</strong>
    73 <dt><strong>Mathematical symbols</strong>
    74 
    74 
    75 <dd>Non-ASCII symbols should be used as appropriate, with some
    75 <dd>Non-ASCII symbols should be used as appropriate, with some
    76 care. In particular, avoid unreadable arrows: <tt>==&gt;</tt> should
    76 care. In particular, avoid unreadable arrows: <tt>==&gt;</tt> should
    77 be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool
    77 be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isabelle
    78 unsymbolize</tt> to clean up the sources.
    78 unsymbolize</tt> to clean up the sources.
    79 
    79 
    80 <p>
    80 <p>
    81 
    81 
    82 The following ASCII symbols of HOL should be generally avoided:
    82 The following ASCII symbols of HOL should be generally avoided: