From: Stefano Zacchiroli Date: Fri, 14 Jul 2006 12:06:30 +0000 (+0000) Subject: snapshot X-Git-Tag: make_still_working~7070 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f08e376eb0b370f92900182d3a5867a5b8c0cf7b;p=helm.git snapshot --- diff --git a/helm/www/matita/Makefile b/helm/www/matita/Makefile index d31130452..6eb664099 100644 --- a/helm/www/matita/Makefile +++ b/helm/www/matita/Makefile @@ -15,6 +15,7 @@ all: @echo "Nothing to do per default, interesting targets:" @echo @echo " manual # import the (xhtml version of the) user manual" + @echo " library # import the scripts building the library" @echo " images # build images for the splash screen" @echo " papers # build the papers page from xml/papers.xml" @echo @@ -29,6 +30,15 @@ manual-stamp: $(DOCS_SRC_DIR)/*.xml $(DOCS_SRC_DIR)/xsl/* $(MAKE) -C $(DOCS_SRC_DIR) install DESTDIR=$(DOCS_DEST_DIR)/ touch $@ +.PHONY: library +library: + if [ -d library/ ] ; then \ + svn update library/ ; \ + else \ + echo "Can't find the scripts, check them out in library/" ; \ + exit 1 ; \ + fi + papers: papers.shtml papers.shtml: xsl/papers2xhtml.xsl xml/papers.xml xsltproc $^ > $@ diff --git a/helm/www/matita/images/folder-apache.png b/helm/www/matita/images/folder-apache.png new file mode 100644 index 000000000..3a9b0bb10 Binary files /dev/null and b/helm/www/matita/images/folder-apache.png differ diff --git a/helm/www/matita/images/matitina-apache.png b/helm/www/matita/images/matitina-apache.png new file mode 100644 index 000000000..a1f50fa56 Binary files /dev/null and b/helm/www/matita/images/matitina-apache.png differ diff --git a/helm/www/matita/images/matitina-apache.svg b/helm/www/matita/images/matitina-apache.svg new file mode 100644 index 000000000..b586e6379 --- /dev/null +++ b/helm/www/matita/images/matitina-apache.svg @@ -0,0 +1,65 @@ + + + + + + + + + image/svg+xml + + + + + + + + + + diff --git a/helm/www/matita/images/matitina.svg b/helm/www/matita/images/matitina.svg new file mode 100644 index 000000000..76cdf9c2e --- /dev/null +++ b/helm/www/matita/images/matitina.svg @@ -0,0 +1,63 @@ + + + + + + + + + image/svg+xml + + + + + + + + + + diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index ce58853f7..33a658479 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -14,31 +14,35 @@ Big Matita label -

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

+

+ Matita (that means pencil in italian) is an experimental, + interactive theorem prover under development at the + Computer Science Department of the + University of Bologna. +

-

+ + +

Matita screenshot: authoring interface - Matita is traditional. Its logical foundation is the - Calculus of (Co)Inductive Constructions (CIC). It can re-use - mathematical concepts produced by other proof assistants (e.g. - Coq) when encoded in an - XML representation of CIC. The - interaction paradigm of Matita is familiar, being inspired by CtCoq and - Proof General. Its - proof language is procedural in the same spirit of LCF.

- -

Matita is innovative:

- diff --git a/helm/www/matita/style.css b/helm/www/matita/style.css index c614becaa..d129be452 100644 --- a/helm/www/matita/style.css +++ b/helm/www/matita/style.css @@ -11,6 +11,7 @@ div.menu { left: 0px; width: 150px; text-align: center; + font-size: 10pt; } div.main { @@ -19,6 +20,7 @@ div.main { left: 150px; width: 650px; padding-left:20px; + font-size: 10pt; } div.news { @@ -81,6 +83,10 @@ ul { list-style-type: square; } +p.spaced { + padding-bottom: 2em; +} + /* menu */ div.menu ul { @@ -136,7 +142,8 @@ ul.wide li { div.topimage { text-align: left; - padding-top: 14px; + padding-top: 28px; + padding-bottom: 28px; } div.bottombar {