Admin/page/main-content/index.content
changeset 10114 b07ed0c2f89f
parent 10050 c8e0bd7a1e9c
child 10162 947b7b8b0a69
equal deleted inserted replaced
10113:a1f8d7d4084b 10114:b07ed0c2f89f
    33 
    33 
    34 <p>
    34 <p>
    35 
    35 
    36 <h2>Obtaining Isabelle</h2>
    36 <h2>Obtaining Isabelle</h2>
    37 
    37 
    38 You get <strong><!-- _GP_ distname --></strong> in the 
       
    39 <a href="dist/index.html">distribution area</a>.
       
    40 
       
    41 <p>
       
    42 
       
    43 The <strong><!-- _GP_ distname --></strong> distribution is available
    38 The <strong><!-- _GP_ distname --></strong> distribution is available
    44 from several <a href="dist/index.html">mirror sites</a>.  It includes
    39 from several <a href="dist/index.html">mirror sites</a>.  It includes
    45 source and binary packages and browsable documentation.
    40 source and binary packages and browsable documentation.
    46 
    41 
    47 <p>
    42 <p>