- moved version.txt.in to the help dir

- added Makefile to generate xhtml and pdf from the docbook manual

diff --git a/matita/dist/version.txt.in b/matita/dist/version.txt.in
deleted file mode 100644 (file)
index c275a8c..0000000
--- a/matita/dist/version.txt.in
+++ /dev/null
@@ -1 +0,0 @@
-@MATITA_VERSION@

diff --git a/matita/help/C/Makefile b/matita/help/C/Makefile
new file mode 100644 (file)
index 0000000..ad3ad64
--- /dev/null
+++ b/matita/help/C/Makefile
@@ -0,0 +1,12 @@
+XSLTPROC=xsltproc
+XHTML_XSL=http://docbook.sourceforge.net/release/xsl/current/xhtml/docbook.xsl
+FO_XSL=http://docbook.sourceforge.net/release/xsl/current/fo/docbook.xsl
+all:
+%.html: %.xml
+       xsltproc $(XHTML_XSL) $< > $@
+%.fo: %.xml
+       xsltproc $(FO_XSL) $< > $@
+%.pdf: %.fo
+       fop $< $@
+clean:
+       rm -f *.html *.fo *.pdf

diff --git a/matita/help/C/intro.xml b/matita/help/C/intro.xml
deleted file mode 100644 (file)
index 5510c8e..0000000
--- a/matita/help/C/intro.xml
+++ /dev/null
@@ -1,15 +0,0 @@
-
-<!-- ============= Introduction ============================== -->
-
-<sect1 id="sec_intro">
-  <title>Introduction</title>
-  <sect2 id="what">
-    <title>What is Matita?</title>
-
-    <para>
-      <application>Matita</application> is a proof assistant for ...
-    </para>
-
-  </sect2>
-</sect1>
-

diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml
index 97b58e572a63c7cf8db2e720b3599adb0ccdb7ac..a0da700e471cecc4f4f72c19e3d1f8805481e8bd 100644 (file)
--- a/matita/help/C/matita.xml
+++ b/matita/help/C/matita.xml
@@ -3,15 +3,16 @@
     "http://www.oasis-open.org/docbook/xml/4.1.2/docbookx.dtd" [
 
   <!ENTITY license SYSTEM "legal.xml">
-  <!ENTITY intro SYSTEM "intro.xml">
-  <!ENTITY terms SYSTEM "terms.xml">
-  <!ENTITY tactics SYSTEM "tactics.xml">
+  <!ENTITY install SYSTEM "sec_install.xml">
+  <!ENTITY intro SYSTEM "sec_intro.xml">
+  <!ENTITY terms SYSTEM "sec_terms.xml">
+  <!ENTITY tactics SYSTEM "sec_tactics.xml">
 
   <!ENTITY manrevision "0">
   <!ENTITY date "February 2006">
   <!ENTITY app "<application>Matita</application>">
   <!ENTITY appname "Matita">
-  <!ENTITY appversion SYSTEM "../../dist/version.txt">
+  <!ENTITY appversion SYSTEM "version.txt">
 ]>
 
 <!-- =============Document Header ============================= -->
@@ -140,6 +141,7 @@
 <!-- ============= Document Body ============================= -->
 
 &intro;
+&install;
 &terms;
 &tactics;
 

diff --git a/matita/help/C/sec_install.xml b/matita/help/C/sec_install.xml
new file mode 100644 (file)
index 0000000..308bf02
--- /dev/null
+++ b/matita/help/C/sec_install.xml
@@ -0,0 +1,27 @@
+
+<!-- ============= Installation ============================== -->
+
+<sect1 id="sec_install">
+  <title>Installation</title>
+
+  <sect2>
+    <title>Installing &appname; from sources</title>
+
+    <para>Currently, the only intended way to install &appname; is starting
+      from its source code.  </para>
+
+    <sect3>
+      <title>Getting the source code</title>
+
+      <para>You can get the &appname; source code in two ways:
+       <orderedlist>
+         <listitem> <para>foo</para> </listitem>
+         <listitem> <para>bar</para> </listitem>
+       </orderedlist>
+      </para>
+      
+    </sect3>
+
+  </sect2>
+</sect1>
+

diff --git a/matita/help/C/sec_intro.xml b/matita/help/C/sec_intro.xml
new file mode 100644 (file)
index 0000000..5510c8e
--- /dev/null
+++ b/matita/help/C/sec_intro.xml
@@ -0,0 +1,15 @@
+
+<!-- ============= Introduction ============================== -->
+
+<sect1 id="sec_intro">
+  <title>Introduction</title>
+  <sect2 id="what">
+    <title>What is Matita?</title>
+
+    <para>
+      <application>Matita</application> is a proof assistant for ...
+    </para>
+
+  </sect2>
+</sect1>
+

diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
new file mode 100644 (file)
index 0000000..a423f37
--- /dev/null
+++ b/matita/help/C/sec_tactics.xml
@@ -0,0 +1,189 @@
+
+<!-- ============ Tactics ====================== -->
+<sect1 id="tactics">
+ <title>Tactics</title>
+
+  <sect2 id="tac_absurd">
+    <title>absurd &lt;term&gt;</title>
+    <para>The tactic <command>absurd</command> </para>
+<para>
+</para>
+  </sect2>
+  <sect2 id="tac_apply">
+    <title>apply &lt;term&gt;</title>
+    <para>The tactic <command>apply</command> </para>
+  </sect2>
+  <sect2 id="tac_assumption">
+    <title>assumption</title>
+    <para>The tactic <command>assumption</command> </para>
+  </sect2>
+  <sect2 id="tac_auto">
+    <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
+    <para>The tactic <command>auto</command> </para>
+  </sect2>
+  <sect2 id="tac_clear">
+    <title>clear &lt;id&gt;</title>
+    <para>The tactic <command>clear</command> </para>
+  </sect2>
+  <sect2 id="tac_clearbody">
+    <title>clearbody &lt;id&gt;</title>
+    <para>The tactic <command>clearbody</command> </para>
+  </sect2>
+  <sect2 id="tac_change">
+    <title>change &lt;pattern&gt; with &lt;term&gt;</title>
+    <para>The tactic <command>change</command> </para>
+  </sect2>
+  <sect2 id="tac_compare">
+    <title>compare &lt;term&gt;</title>
+    <para>The tactic <command>compare</command> </para>
+  </sect2>
+  <sect2 id="tac_constructor">
+    <title>constructor &lt;int&gt;</title>
+    <para>The tactic <command>constructor</command> </para>
+  </sect2>
+  <sect2 id="tac_contradiction">
+    <title>contradiction</title>
+    <para>The tactic <command>contradiction</command> </para>
+  </sect2>
+  <sect2 id="tac_cut">
+    <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
+    <para>The tactic <command>cut</command> </para>
+  </sect2>
+  <sect2 id="tac_decide_equality">
+    <title>decide</title>
+    <para>The tactic <command>decide equality</command> </para>
+  </sect2>
+  <sect2 id="tac_decompose">
+    <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
+    <para>The tactic <command>decompose</command> </para>
+  </sect2>
+  <sect2 id="tac_discriminate">
+    <title>discriminate &lt;term&gt;</title>
+    <para>The tactic <command>discriminate</command> </para>
+  </sect2>
+  <sect2 id="tac_elim">
+    <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
+    <para>The tactic <command>elim</command> </para>
+  </sect2>
+  <sect2 id="tac_elimType">
+    <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
+    <para>The tactic <command>elimType</command> </para>
+  </sect2>
+  <sect2 id="tac_exact">
+    <title>exact &lt;term&gt;</title>
+    <para>The tactic <command>exact</command> </para>
+  </sect2>
+  <sect2 id="tac_exists">
+    <title>exists</title>
+    <para>The tactic <command>exists</command> </para>
+  </sect2>
+  <sect2 id="tac_fail">
+    <title>fail</title>
+    <para>The tactic <command>fail</command> </para>
+  </sect2>
+  <sect2 id="tac_fold">
+    <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
+    <para>The tactic <command>fold</command> </para>
+  </sect2>
+  <sect2 id="tac_fourier">
+    <title>fourier</title>
+    <para>The tactic <command>fourier</command> </para>
+  </sect2>
+  <sect2 id="tac_fwd">
+    <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
+    <para>The tactic <command>fwd</command> </para>
+  </sect2>
+  <sect2 id="tac_generalize">
+    <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
+    <para>The tactic <command>generalize</command> </para>
+  </sect2>
+  <sect2 id="tac_id">
+    <title>id</title>
+    <para>The tactic <command>id</command> </para>
+  </sect2>
+  <sect2 id="tac_injection">
+    <title>injection &lt;term&gt;</title>
+    <para>The tactic <command>injection</command> </para>
+  </sect2>
+  <sect2 id="tac_intro">
+    <title>intro [&lt;ident&gt;]</title>
+    <para>The tactic <command>intro</command> </para>
+  </sect2>
+  <sect2 id="tac_intros">
+    <title>intros &lt;intros_spec&gt;</title>
+    <para>The tactic <command>intros</command> </para>
+  </sect2>
+  <sect2 id="tac_inversion">
+    <title>intros &lt;term&gt;</title>
+    <para>The tactic <command>intros</command> </para>
+  </sect2>
+  <sect2 id="tac_lapply">
+    <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
+    <para>The tactic <command>lapply</command> </para>
+  </sect2>
+  <sect2 id="tac_left">
+    <title>left</title>
+    <para>The tactic <command>left</command> </para>
+  </sect2>
+  <sect2 id="tac_letin">
+    <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
+    <para>The tactic <command>letin</command> </para>
+  </sect2>
+  <sect2 id="tac_normalize">
+    <title>normalize &lt;pattern&gt;</title>
+    <para>The tactic <command>normalize</command> </para>
+  </sect2>
+  <sect2 id="tac_paramodulation">
+    <title>paramodulation &lt;pattern&gt;</title>
+    <para>The tactic <command>paramodulation</command> </para>
+  </sect2>
+  <sect2 id="tac_reduce">
+    <title>reduce &lt;pattern&gt;</title>
+    <para>The tactic <command>reduce</command> </para>
+  </sect2>
+  <sect2 id="tac_reflexivity">
+    <title>reflexivity</title>
+    <para>The tactic <command>reflexivity</command> </para>
+  </sect2>
+  <sect2 id="tac_replace">
+    <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
+    <para>The tactic <command>replace</command> </para>
+  </sect2>
+  <sect2 id="tac_rewrite">
+    <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
+    <para>The tactic <command>rewrite</command> </para>
+  </sect2>
+  <sect2 id="tac_right">
+    <title>right</title>
+    <para>The tactic <command>right</command> </para>
+  </sect2>
+  <sect2 id="tac_ring">
+    <title>ring</title>
+    <para>The tactic <command>ring</command> </para>
+  </sect2>
+  <sect2 id="tac_simplify">
+    <title>simplify &lt;pattern&gt;</title>
+    <para>The tactic <command>simplify</command> </para>
+  </sect2>
+  <sect2 id="tac_split">
+    <title>split</title>
+    <para>The tactic <command>split</command> </para>
+  </sect2>
+  <sect2 id="tac_symmetry">
+    <title>symmetry</title>
+    <para>The tactic <command>symmetry</command> </para>
+  </sect2>
+  <sect2 id="tac_transitivity">
+    <title>transitivity &lt;term&gt;</title>
+    <para>The tactic <command>transitivity</command> </para>
+  </sect2>
+  <sect2 id="tac_unfold">
+    <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
+    <para>The tactic <command>unfold</command> </para>
+  </sect2>
+  <sect2 id="tac_whd">
+    <title>whd &lt;pattern&gt;</title>
+    <para>The tactic <command>whd</command> </para>
+  </sect2>
+
+</sect1>

diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml
new file mode 100644 (file)
index 0000000..d92518d
--- /dev/null
+++ b/matita/help/C/sec_terms.xml
@@ -0,0 +1,28 @@
+
+<!-- =========== Terms, declarations and definitions ============ -->
+
+<sect1 id="sec_terms">
+  <title>Terms, definitions, declarations and proofs</title>
+
+  <sect2 id="terms">
+    <title>Terms</title>
+    <para> TODO </para>
+  </sect2>
+
+  <sect2 id="definitions">
+    <title>Definitions</title>
+    <para> TODO </para>
+  </sect2>
+
+  <sect2 id="declarations">
+    <title>Declarations (of inductive types)</title>
+    <para> TODO </para>
+  </sect2>
+
+  <sect2 id="proofs">
+    <title>Proofs</title>
+    <para> TODO </para>
+  </sect2>
+
+</sect1>
+

diff --git a/matita/help/C/tactics.xml b/matita/help/C/tactics.xml
deleted file mode 100644 (file)
index a423f37..0000000
--- a/matita/help/C/tactics.xml
+++ /dev/null
@@ -1,189 +0,0 @@
-
-<!-- ============ Tactics ====================== -->
-<sect1 id="tactics">
- <title>Tactics</title>
-
-  <sect2 id="tac_absurd">
-    <title>absurd &lt;term&gt;</title>
-    <para>The tactic <command>absurd</command> </para>
-<para>
-</para>
-  </sect2>
-  <sect2 id="tac_apply">
-    <title>apply &lt;term&gt;</title>
-    <para>The tactic <command>apply</command> </para>
-  </sect2>
-  <sect2 id="tac_assumption">
-    <title>assumption</title>
-    <para>The tactic <command>assumption</command> </para>
-  </sect2>
-  <sect2 id="tac_auto">
-    <title>auto [depth=&lt;int&gt;] [width=&lt;int&gt;] [paramodulation] [full]</title>
-    <para>The tactic <command>auto</command> </para>
-  </sect2>
-  <sect2 id="tac_clear">
-    <title>clear &lt;id&gt;</title>
-    <para>The tactic <command>clear</command> </para>
-  </sect2>
-  <sect2 id="tac_clearbody">
-    <title>clearbody &lt;id&gt;</title>
-    <para>The tactic <command>clearbody</command> </para>
-  </sect2>
-  <sect2 id="tac_change">
-    <title>change &lt;pattern&gt; with &lt;term&gt;</title>
-    <para>The tactic <command>change</command> </para>
-  </sect2>
-  <sect2 id="tac_compare">
-    <title>compare &lt;term&gt;</title>
-    <para>The tactic <command>compare</command> </para>
-  </sect2>
-  <sect2 id="tac_constructor">
-    <title>constructor &lt;int&gt;</title>
-    <para>The tactic <command>constructor</command> </para>
-  </sect2>
-  <sect2 id="tac_contradiction">
-    <title>contradiction</title>
-    <para>The tactic <command>contradiction</command> </para>
-  </sect2>
-  <sect2 id="tac_cut">
-    <title>cut &lt;term&gt; [as &lt;id&gt;]</title>
-    <para>The tactic <command>cut</command> </para>
-  </sect2>
-  <sect2 id="tac_decide_equality">
-    <title>decide</title>
-    <para>The tactic <command>decide equality</command> </para>
-  </sect2>
-  <sect2 id="tac_decompose">
-    <title>decompose [&lt;ident list&gt;] &lt;ident&gt; [&lt;intros_spec&gt;]</title>
-    <para>The tactic <command>decompose</command> </para>
-  </sect2>
-  <sect2 id="tac_discriminate">
-    <title>discriminate &lt;term&gt;</title>
-    <para>The tactic <command>discriminate</command> </para>
-  </sect2>
-  <sect2 id="tac_elim">
-    <title>elim &lt;term&gt; [using &lt;term&gt;] [&lt;intros_spec&gt;]</title>
-    <para>The tactic <command>elim</command> </para>
-  </sect2>
-  <sect2 id="tac_elimType">
-    <title>elimType &lt;term&gt; [using &lt;term&gt;]</title>
-    <para>The tactic <command>elimType</command> </para>
-  </sect2>
-  <sect2 id="tac_exact">
-    <title>exact &lt;term&gt;</title>
-    <para>The tactic <command>exact</command> </para>
-  </sect2>
-  <sect2 id="tac_exists">
-    <title>exists</title>
-    <para>The tactic <command>exists</command> </para>
-  </sect2>
-  <sect2 id="tac_fail">
-    <title>fail</title>
-    <para>The tactic <command>fail</command> </para>
-  </sect2>
-  <sect2 id="tac_fold">
-    <title>fold &lt;reduction_kind&gt; &lt;term&gt; &lt;pattern&gt;</title>
-    <para>The tactic <command>fold</command> </para>
-  </sect2>
-  <sect2 id="tac_fourier">
-    <title>fourier</title>
-    <para>The tactic <command>fourier</command> </para>
-  </sect2>
-  <sect2 id="tac_fwd">
-    <title>fwd &lt;ident&gt; [&lt;ident list&gt;]</title>
-    <para>The tactic <command>fwd</command> </para>
-  </sect2>
-  <sect2 id="tac_generalize">
-    <title>generalize &lt;pattern&gt; [as &lt;id&gt;]</title>
-    <para>The tactic <command>generalize</command> </para>
-  </sect2>
-  <sect2 id="tac_id">
-    <title>id</title>
-    <para>The tactic <command>id</command> </para>
-  </sect2>
-  <sect2 id="tac_injection">
-    <title>injection &lt;term&gt;</title>
-    <para>The tactic <command>injection</command> </para>
-  </sect2>
-  <sect2 id="tac_intro">
-    <title>intro [&lt;ident&gt;]</title>
-    <para>The tactic <command>intro</command> </para>
-  </sect2>
-  <sect2 id="tac_intros">
-    <title>intros &lt;intros_spec&gt;</title>
-    <para>The tactic <command>intros</command> </para>
-  </sect2>
-  <sect2 id="tac_inversion">
-    <title>intros &lt;term&gt;</title>
-    <para>The tactic <command>intros</command> </para>
-  </sect2>
-  <sect2 id="tac_lapply">
-    <title>lapply [depth=&lt;int&gt;] &lt;term&gt; [to &lt;term list] [using &lt;ident&gt;]</title>
-    <para>The tactic <command>lapply</command> </para>
-  </sect2>
-  <sect2 id="tac_left">
-    <title>left</title>
-    <para>The tactic <command>left</command> </para>
-  </sect2>
-  <sect2 id="tac_letin">
-    <title>letin &lt;ident&gt; ≝ &lt;term&gt;</title>
-    <para>The tactic <command>letin</command> </para>
-  </sect2>
-  <sect2 id="tac_normalize">
-    <title>normalize &lt;pattern&gt;</title>
-    <para>The tactic <command>normalize</command> </para>
-  </sect2>
-  <sect2 id="tac_paramodulation">
-    <title>paramodulation &lt;pattern&gt;</title>
-    <para>The tactic <command>paramodulation</command> </para>
-  </sect2>
-  <sect2 id="tac_reduce">
-    <title>reduce &lt;pattern&gt;</title>
-    <para>The tactic <command>reduce</command> </para>
-  </sect2>
-  <sect2 id="tac_reflexivity">
-    <title>reflexivity</title>
-    <para>The tactic <command>reflexivity</command> </para>
-  </sect2>
-  <sect2 id="tac_replace">
-    <title>replace &lt;pattern&gt; with &lt;term&gt;</title>
-    <para>The tactic <command>replace</command> </para>
-  </sect2>
-  <sect2 id="tac_rewrite">
-    <title>rewrite {&lt;|&gt;} &lt;term&gt; &lt;pattern&gt;</title>
-    <para>The tactic <command>rewrite</command> </para>
-  </sect2>
-  <sect2 id="tac_right">
-    <title>right</title>
-    <para>The tactic <command>right</command> </para>
-  </sect2>
-  <sect2 id="tac_ring">
-    <title>ring</title>
-    <para>The tactic <command>ring</command> </para>
-  </sect2>
-  <sect2 id="tac_simplify">
-    <title>simplify &lt;pattern&gt;</title>
-    <para>The tactic <command>simplify</command> </para>
-  </sect2>
-  <sect2 id="tac_split">
-    <title>split</title>
-    <para>The tactic <command>split</command> </para>
-  </sect2>
-  <sect2 id="tac_symmetry">
-    <title>symmetry</title>
-    <para>The tactic <command>symmetry</command> </para>
-  </sect2>
-  <sect2 id="tac_transitivity">
-    <title>transitivity &lt;term&gt;</title>
-    <para>The tactic <command>transitivity</command> </para>
-  </sect2>
-  <sect2 id="tac_unfold">
-    <title>unfold [&lt;term&gt;] &lt;pattern&gt;</title>
-    <para>The tactic <command>unfold</command> </para>
-  </sect2>
-  <sect2 id="tac_whd">
-    <title>whd &lt;pattern&gt;</title>
-    <para>The tactic <command>whd</command> </para>
-  </sect2>
-
-</sect1>

diff --git a/matita/help/C/terms.xml b/matita/help/C/terms.xml
deleted file mode 100644 (file)
index d92518d..0000000
--- a/matita/help/C/terms.xml
+++ /dev/null
@@ -1,28 +0,0 @@
-
-<!-- =========== Terms, declarations and definitions ============ -->
-
-<sect1 id="sec_terms">
-  <title>Terms, definitions, declarations and proofs</title>
-
-  <sect2 id="terms">
-    <title>Terms</title>
-    <para> TODO </para>
-  </sect2>
-
-  <sect2 id="definitions">
-    <title>Definitions</title>
-    <para> TODO </para>
-  </sect2>
-
-  <sect2 id="declarations">
-    <title>Declarations (of inductive types)</title>
-    <para> TODO </para>
-  </sect2>
-
-  <sect2 id="proofs">
-    <title>Proofs</title>
-    <para> TODO </para>
-  </sect2>
-
-</sect1>
-

diff --git a/matita/help/C/version.txt.in b/matita/help/C/version.txt.in
new file mode 100644 (file)
index 0000000..c275a8c
--- /dev/null
+++ b/matita/help/C/version.txt.in
@@ -0,0 +1 @@
+@MATITA_VERSION@