diff options
author | 2002-07-13 16:29:53 +0000 | |
---|---|---|
committer | 2002-07-13 16:29:53 +0000 | |
commit | 54f652a05b0c7995d4385f4139009f299b36bc45 (patch) | |
tree | 976b64b90e3491a0024a5c1251d540f140472fc0 /html/screenshot.html | |
parent | 9c076cb3a0fd5658ff33e543e3de3b45bc320c20 (diff) |
Fix layout a bit
Diffstat (limited to 'html/screenshot.html')
-rw-r--r-- | html/screenshot.html | 47 |
1 files changed, 27 insertions, 20 deletions
diff --git a/html/screenshot.html b/html/screenshot.html index 3cf0ccae..6cce9e3a 100644 --- a/html/screenshot.html +++ b/html/screenshot.html @@ -3,12 +3,9 @@ Here are some screenshots of Proof General 3.0 running with different theorem provers. To see the full-size version of a picture, click on its thumbnail. </p> -<p> -<i>NB: Your browser needs PNG support to view these pictures. -</i> -</p> -<!-- todo: php3 this, add space between rows! --> +<!-- FIXME: update pictures. Fix vertical centering of screenshots. --> + <table width="80%"> <tr> <td width="200"> @@ -17,7 +14,7 @@ of a picture, click on its thumbnail. </a> </td> <td> -<p> +<p><font size="-1"> Building a simple proof in LEGO with proof-by-pointing. <br> The top half of the window displays the proof script. @@ -29,8 +26,10 @@ has a blue background. <br> Clicking on terms in the subgoals list generates commands which are added to the proof script. -</p> -</tr> +</font></p> +<br> +</td></tr> + <tr> <td width="200"> <a href="images/pg-coq-screenshot.png"> @@ -38,7 +37,7 @@ commands which are added to the proof script. </a> </td> <td> -<p> +<p><font size="-1"> Coq Proof General running in multiple frame mode, full screen shot (1024x768). <br> @@ -49,8 +48,10 @@ indication that Coq is processing the induction step, because the background of the proof step is pink. It will become blue when Coq finishes that step. -</p> -</tr> +</font></p> +</br> +</td></tr> + <tr> <td width="200"> <a href="images/pg-isa-screenshot.png"> @@ -58,7 +59,7 @@ blue when Coq finishes that step. </a> </td> <td> -<p> +<p><font size="-1"> Replaying a domain theory proof in Isabelle's HOLCF logic. <br> In Isabelle, theory files as well as ML files are coloured. @@ -71,8 +72,10 @@ display as symbols using the <a href="http://x-symbol.sourceforge.net/">X-Symbol</a> package in conjunction with Proof General. Here you can see some symbols in Isabelle's output. -</p> -</tr> +</font></p> +</br> +</td></tr> + <tr> <td width="200"> <a href="images/pg-isar-screenshot.png"> @@ -80,11 +83,13 @@ Here you can see some symbols in Isabelle's output. </a> </td> <td> -<p> -Replaying a proof in Isar, Isabelle's new proof language +<p><font size="-1"> +Replaying a proof in Isar, Isabelle's declarative proof language developed by Markus Wenzel. -</p> -</tr> +</font></p> +<br> +</td></tr> + <tr> <td width="200"> <a href="images/pg-lego-console.png"> @@ -92,13 +97,15 @@ developed by Markus Wenzel. </a> </td> <td> -<p> +<p><font size="-1"> LEGO Proof General running in plain console mode. <br> This shows that you can run Proof General even if sometimes you need to use a plain tty or xterminal. Of course, the graphical features are reduced! -</p> +</font></p> +<br> +</td> </tr> </table> |