X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fdist%2FREADME;fp=matita%2Fdist%2FREADME;h=a27350d32802276aaf80fbfe75c57e547405afb7;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/dist/README b/matita/dist/README
new file mode 100644
index 000000000..a27350d32
--- /dev/null
+++ b/matita/dist/README
@@ -0,0 +1,53 @@
+
+MATITA
+------
+
+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). It can re-use mathematical concepts produced by other
+proof assistants like Coq and encoded in an XML encoding 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:
+
+- the user interface sports high quality bidimensional rendering of proofs and
+  formulae transformed on-the-fly to MathML markup, on which direct
+  manipulation of the underlying CIC terms is still possible;
+
+- the knowledge base is distributed: every authored concepts can be published
+  becoming 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.
+
+More information are available on the Matita web site:
+
+  http://matita.cs.unibo.it/
+
+
+INSTALLATION
+------------
+
+See the file INSTALL for building and installation instructions.
+
+
+BUGS
+----
+
+Bugs reporting is handled using the Bugzilla bug tracker available at:
+
+  http://bugs.mowgli.cs.unibo.it/
+
+
+LICENSE
+-------
+
+Matita and its documentation are free software.
+See the file COPYING for copying conditions.
+