--- a/Admin/website/overview.html Mon Jun 06 11:30:57 2005 +0200
+++ b/Admin/website/overview.html Mon Jun 06 12:17:59 2005 +0200
@@ -35,13 +35,20 @@
(University of Cambridge, UK) and Tobias Nipkow (Technical
University of Munich, Germany).</p>
- <h2>What Isabelle offers</h2>
+ <h2>Preview on Isabelle</h2>
- <a href="//img/isabelle_pg_screenshot_big.png">
+ <a href="//media/pg_preview.mov">
<img class="left" src="//img/isabelle_pg_screenshot_small.png" alt="Sreenshot "
width="250" height="277" />
</a>
+ <p>Here is a <a href="//media/pg_preview.mov">hyperlinked preview</a> demonstrating
+ Isabelle and ProofGeneral, in <a href="http://www.apple.com/quicktime/download/">QuickTime
+ format</a>, and also as a <a href="//media/pg_preview.pdf">non-hyperlinked preview</a> in PDF.</p>
+ <br clear="all"/>
+
+ <h2>What Isabelle offers</h2>
+
<p>Isabelle provides excellent notational support: new notations
can be introduced, using normal mathematical symbols. Proofs can
be written in a structured notation based upon traditional proof
@@ -75,17 +82,11 @@
eases the task of writing and maintaining proof scripts.</p>
<br clear="all" />
- <h2>Preview</h2>
-
- <p>We provide a <a href="media/pg_preview.mov">hyperlinked preview</a> demonstrating
- Isabelle and ProofGeneral, in <a href="http://www.apple.com/quicktime/download/">QuickTime
- format</a>, and also as a <a href="media/pg_preview.pdf">non-hyperlinked preview</a> in PDF.</p>
-
<p>Ample <a href="dist/documentation.html">documentation</a> is available
about using Isabelle and its inner concepts, including a
<a href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
Springer-Verlag.</p>
-
+
<h2>Projects</h2>
<p>There is an (incomplete) list of past and present <a href=