Admin/website/overview.html
changeset 16674 bf2cd93cc245
parent 16619 94e3d94b426d
child 17563 abb280dd3431
equal deleted inserted replaced
16673:6b14aba5ddaa 16674:bf2cd93cc245
    12     <?include file="//include/header.include.html"?>
    12     <?include file="//include/header.include.html"?>
    13     <div class="hr"><hr/></div>
    13     <div class="hr"><hr/></div>
    14     <?include file="//include/navigation.include.html"?>
    14     <?include file="//include/navigation.include.html"?>
    15     <div class="hr"><hr/></div>
    15     <div class="hr"><hr/></div>
    16     <div id="content">
    16     <div id="content">
    17       <?include file="//include/mirrorlist.major.include.html"?>
    17 
    18       <div class="hr"><hr/></div>
       
    19       <h2>What is Isabelle?</h2> 
    18       <h2>What is Isabelle?</h2> 
    20       <p>
    19       <p>
    21       Isabelle is a generic proof assistant. It allows mathematical
    20       Isabelle is a generic proof assistant. It allows mathematical
    22       formulas to be expressed in a formal language and provides tools
    21       formulas to be expressed in a formal language and provides tools
    23       for proving those formulas in a logical calculus.  The main
    22       for proving those formulas in a logical calculus.  The main
    37       (University of Cambridge, UK) and Tobias Nipkow (Technical
    36       (University of Cambridge, UK) and Tobias Nipkow (Technical
    38       University of Munich, Germany).</p>
    37       University of Munich, Germany).</p>
    39 
    38 
    40       <p>Isabelle is distributed <em>freely</em> under the open source
    39       <p>Isabelle is distributed <em>freely</em> under the open source
    41       <!--a href="//dist/packages/Isabelle/COPYRIGHT"-->BSD license<!--/a-->.
    40       <!--a href="//dist/packages/Isabelle/COPYRIGHT"-->BSD license<!--/a-->.
    42       You may use any of our <a href="dist/index.html">mirrors</a> for download.</p>
    41       You may use any of our <a href="mirrors.html">mirrors</a> for download.</p>
    43 
    42 
    44       <h2>Preview of Isabelle</h2>
    43       <h2>Preview of Isabelle</h2>
    45 
    44 
    46         <a href="//media/pg_preview.mov">
    45         <a href="//media/pg_preview.mov">
    47             <img class="left" src="//img/isabelle_pg_screenshot_small.png" alt="Sreenshot "
    46             <img class="left" src="//img/isabelle_pg_screenshot_small.png" alt="Sreenshot "
    85       
    84       
    86       <p>Isabelle is closely integrated with the <a href=
    85       <p>Isabelle is closely integrated with the <a href=
    87       "http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> user interface, which
    86       "http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> user interface, which
    88       eases the task of writing and maintaining proof scripts.</p>
    87       eases the task of writing and maintaining proof scripts.</p>
    89 
    88 
    90       <p>Ample <a href="dist/documentation.html">documentation</a> is available
    89       <p>Ample <a href="documentation.html">documentation</a> is available
    91       about using Isabelle and its inner concepts, including a
    90       about using Isabelle and its inner concepts, including a
    92       <a href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
    91       <a href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
    93       Springer-Verlag.</p>
    92       Springer-Verlag.</p>
    94 
    93 
    95     </div>
    94     </div>