equal
deleted
inserted
replaced
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> |