From: Stefano Zacchiroli Date: Fri, 9 Jun 2006 23:52:36 +0000 (+0000) Subject: - added a real-life index page X-Git-Tag: make_still_working~7237 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0775f6acafa9aa176d148a8f3acf7e750c1c3171;p=helm.git - added a real-life index page - removed the label 'matita' on the top-left logo - added a big 'matita' label for the index page - factorized common stuff that goes inside in a new SSI --- diff --git a/helm/www/matita/community.shtml b/helm/www/matita/community.shtml index 1dfd479fa..16e029f73 100644 --- a/helm/www/matita/community.shtml +++ b/helm/www/matita/community.shtml @@ -1,8 +1,8 @@ - Matita home page - community - + Matita - Community + diff --git a/helm/www/matita/development.shtml b/helm/www/matita/development.shtml index 193be32a0..829e4713d 100644 --- a/helm/www/matita/development.shtml +++ b/helm/www/matita/development.shtml @@ -1,12 +1,13 @@ - Matita home page - developers - + Matita - Development +

Matita Development

The origins of Matita go back to 1999 and are intertwined with the @@ -15,8 +16,9 @@ Matita what it looks today. In this page we tried to summarize all of them, we apologize for whom we forgot to mention.

Current team members

Andrea Asperti - Full Professor
Claudio Sacerdoti Coen - Lecturer
Enrico Tassi - PhD Student

Former members

Ferruccio Guidi - PhD
Luca Padovani - Lecturer
Irene Schena - PhD
Matteo Selmi - Master Student
Vincenzo Tamburrelli - Master Student

diff --git a/helm/www/matita/documentation.shtml b/helm/www/matita/documentation.shtml index 7718cf4cc..293520143 100644 --- a/helm/www/matita/documentation.shtml +++ b/helm/www/matita/documentation.shtml @@ -1,8 +1,8 @@ - Matita home page - documentation - + Matita - Documentation + diff --git a/helm/www/matita/download.shtml b/helm/www/matita/download.shtml index 94ec8dc6a..b992b2694 100644 --- a/helm/www/matita/download.shtml +++ b/helm/www/matita/download.shtml @@ -1,8 +1,8 @@ - Matita home page - download - + Matita - Download + diff --git a/helm/www/matita/images/matita-small.png b/helm/www/matita/images/matita-small.png index f6a234f2a..15b5ac691 100644 Binary files a/helm/www/matita/images/matita-small.png and b/helm/www/matita/images/matita-small.png differ diff --git a/helm/www/matita/images/matita-text-big.png b/helm/www/matita/images/matita-text-big.png new file mode 100644 index 000000000..b76d87446 Binary files /dev/null and b/helm/www/matita/images/matita-text-big.png differ diff --git a/helm/www/matita/images/matita-w-text-big.png b/helm/www/matita/images/matita-w-text-big.png new file mode 100644 index 000000000..f7e8a5e07 Binary files /dev/null and b/helm/www/matita/images/matita-w-text-big.png differ diff --git a/helm/www/matita/images/matita-w-text-small.png b/helm/www/matita/images/matita-w-text-small.png new file mode 100644 index 000000000..f6a234f2a Binary files /dev/null and b/helm/www/matita/images/matita-w-text-small.png differ diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index 6ef651759..3a69a1d72 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -1,66 +1,51 @@ - - Matita home page - - +

Matita is a new document-centric interactive theorem prover that + integrates several Mathematical Knowledge + Management tools and techniques.

- +

Matita is traditional. Its logical foundation is the + Calculus of (Co)Inductive Constructions (CIC), and it can re-use + mathematical concepts produced by other proof assistants like + Coq and encoded in an + XML dialect. The interaction + paradigm of Matita is well known, having been inspired by + Proof General, and its + proof language is procedural in the same spirit of LCF.

+ +

Matita is innovative:

its user interface sports high quality bidimensional rendering of + proofs and formulae exploiting + MathML markup, equipped with + direct manipulation of the underlying CIC terms;
its library is distributed: every authored concepts can be + published and become part of the Matita library which can be browsed as + an hypertext (locally or on the World Wide Web) and searched by means of + content-based queries;
the tactical language, part of the proof language, has + step-by-step semantics, enabling inspection and replaying of deeply + structured proof scripts

1. Developers
2. Documentation
3. Community
4. Download

- + +

diff --git a/helm/www/matita/menubar.shtml b/helm/www/matita/menubar.shtml index 8e0043a49..62e98c212 100644 --- a/helm/www/matita/menubar.shtml +++ b/helm/www/matita/menubar.shtml @@ -1,5 +1,4 @@

Matita Home
Documentation

Matita - Splash

+ +

1. Developers
2. Documentation
3. Community
4. Download

+ + + + diff --git a/helm/www/matita/style.css b/helm/www/matita/style.css index 67b4cf03b..3f36a507e 100644 --- a/helm/www/matita/style.css +++ b/helm/www/matita/style.css @@ -36,10 +36,21 @@ div.main h4 { color: #808080; } -p { +ul { + list-style-type: square; } -ul { +div.menu { + position: absolute; + left: 0px; + width: 150px; + padding-top: 110px; + background: url(images/matita-small.png); + background-repeat: no-repeat; + background-position: 1cm top; +} + +div.menu ul { list-style-type: none; } @@ -63,6 +74,10 @@ a.menu:hover { background-color: #ecf6f9; } +ul.wide li { + padding-bottom: 5px; +} + a { margin: 2px; color: #591622; @@ -74,16 +89,6 @@ a:hover { background-color: #ecf6f9; } -div.menu { - position: absolute; - left: 0px; - width: 150px; - padding-top: 140px; - background: url(images/matita-small.png); - background-repeat: no-repeat; - background-position: 1cm top; -} - div.main { position: absolute; top: 0px; @@ -91,6 +96,15 @@ div.main { width: 650px; } +.center { + text-align: center; +} + +div.topimage { + text-align: center; + padding-top: 14px; +} + div.bottombar { display: block; width: auto; @@ -122,3 +136,10 @@ pre.code { font-size: 95%; } +div.logo { + background: url(images/matita-big.png); + background-repeat: no-repeat; + background-position: center top; + height: 600px; +} + diff --git a/helm/www/matita/xhtml-meta.shtml b/helm/www/matita/xhtml-meta.shtml new file mode 100644 index 000000000..ebed9ee6f --- /dev/null +++ b/helm/www/matita/xhtml-meta.shtml @@ -0,0 +1 @@ +