+++ /dev/null
-@MATITA_VERSION@
--- /dev/null
+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
+++ /dev/null
-
-<!-- ============= 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>
-
"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 ============================= -->
<!-- ============= Document Body ============================= -->
&intro;
+&install;
&terms;
&tactics;
--- /dev/null
+
+<!-- ============= 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>
+
--- /dev/null
+
+<!-- ============= 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>
+
--- /dev/null
+
+<!-- ============ Tactics ====================== -->
+<sect1 id="tactics">
+ <title>Tactics</title>
+
+ <sect2 id="tac_absurd">
+ <title>absurd <term></title>
+ <para>The tactic <command>absurd</command> </para>
+<para>
+</para>
+ </sect2>
+ <sect2 id="tac_apply">
+ <title>apply <term></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=<int>] [width=<int>] [paramodulation] [full]</title>
+ <para>The tactic <command>auto</command> </para>
+ </sect2>
+ <sect2 id="tac_clear">
+ <title>clear <id></title>
+ <para>The tactic <command>clear</command> </para>
+ </sect2>
+ <sect2 id="tac_clearbody">
+ <title>clearbody <id></title>
+ <para>The tactic <command>clearbody</command> </para>
+ </sect2>
+ <sect2 id="tac_change">
+ <title>change <pattern> with <term></title>
+ <para>The tactic <command>change</command> </para>
+ </sect2>
+ <sect2 id="tac_compare">
+ <title>compare <term></title>
+ <para>The tactic <command>compare</command> </para>
+ </sect2>
+ <sect2 id="tac_constructor">
+ <title>constructor <int></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 <term> [as <id>]</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 [<ident list>] <ident> [<intros_spec>]</title>
+ <para>The tactic <command>decompose</command> </para>
+ </sect2>
+ <sect2 id="tac_discriminate">
+ <title>discriminate <term></title>
+ <para>The tactic <command>discriminate</command> </para>
+ </sect2>
+ <sect2 id="tac_elim">
+ <title>elim <term> [using <term>] [<intros_spec>]</title>
+ <para>The tactic <command>elim</command> </para>
+ </sect2>
+ <sect2 id="tac_elimType">
+ <title>elimType <term> [using <term>]</title>
+ <para>The tactic <command>elimType</command> </para>
+ </sect2>
+ <sect2 id="tac_exact">
+ <title>exact <term></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 <reduction_kind> <term> <pattern></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 <ident> [<ident list>]</title>
+ <para>The tactic <command>fwd</command> </para>
+ </sect2>
+ <sect2 id="tac_generalize">
+ <title>generalize <pattern> [as <id>]</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 <term></title>
+ <para>The tactic <command>injection</command> </para>
+ </sect2>
+ <sect2 id="tac_intro">
+ <title>intro [<ident>]</title>
+ <para>The tactic <command>intro</command> </para>
+ </sect2>
+ <sect2 id="tac_intros">
+ <title>intros <intros_spec></title>
+ <para>The tactic <command>intros</command> </para>
+ </sect2>
+ <sect2 id="tac_inversion">
+ <title>intros <term></title>
+ <para>The tactic <command>intros</command> </para>
+ </sect2>
+ <sect2 id="tac_lapply">
+ <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</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 <ident> ≝ <term></title>
+ <para>The tactic <command>letin</command> </para>
+ </sect2>
+ <sect2 id="tac_normalize">
+ <title>normalize <pattern></title>
+ <para>The tactic <command>normalize</command> </para>
+ </sect2>
+ <sect2 id="tac_paramodulation">
+ <title>paramodulation <pattern></title>
+ <para>The tactic <command>paramodulation</command> </para>
+ </sect2>
+ <sect2 id="tac_reduce">
+ <title>reduce <pattern></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 <pattern> with <term></title>
+ <para>The tactic <command>replace</command> </para>
+ </sect2>
+ <sect2 id="tac_rewrite">
+ <title>rewrite {<|>} <term> <pattern></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 <pattern></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 <term></title>
+ <para>The tactic <command>transitivity</command> </para>
+ </sect2>
+ <sect2 id="tac_unfold">
+ <title>unfold [<term>] <pattern></title>
+ <para>The tactic <command>unfold</command> </para>
+ </sect2>
+ <sect2 id="tac_whd">
+ <title>whd <pattern></title>
+ <para>The tactic <command>whd</command> </para>
+ </sect2>
+
+</sect1>
--- /dev/null
+
+<!-- =========== 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>
+
+++ /dev/null
-
-<!-- ============ Tactics ====================== -->
-<sect1 id="tactics">
- <title>Tactics</title>
-
- <sect2 id="tac_absurd">
- <title>absurd <term></title>
- <para>The tactic <command>absurd</command> </para>
-<para>
-</para>
- </sect2>
- <sect2 id="tac_apply">
- <title>apply <term></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=<int>] [width=<int>] [paramodulation] [full]</title>
- <para>The tactic <command>auto</command> </para>
- </sect2>
- <sect2 id="tac_clear">
- <title>clear <id></title>
- <para>The tactic <command>clear</command> </para>
- </sect2>
- <sect2 id="tac_clearbody">
- <title>clearbody <id></title>
- <para>The tactic <command>clearbody</command> </para>
- </sect2>
- <sect2 id="tac_change">
- <title>change <pattern> with <term></title>
- <para>The tactic <command>change</command> </para>
- </sect2>
- <sect2 id="tac_compare">
- <title>compare <term></title>
- <para>The tactic <command>compare</command> </para>
- </sect2>
- <sect2 id="tac_constructor">
- <title>constructor <int></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 <term> [as <id>]</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 [<ident list>] <ident> [<intros_spec>]</title>
- <para>The tactic <command>decompose</command> </para>
- </sect2>
- <sect2 id="tac_discriminate">
- <title>discriminate <term></title>
- <para>The tactic <command>discriminate</command> </para>
- </sect2>
- <sect2 id="tac_elim">
- <title>elim <term> [using <term>] [<intros_spec>]</title>
- <para>The tactic <command>elim</command> </para>
- </sect2>
- <sect2 id="tac_elimType">
- <title>elimType <term> [using <term>]</title>
- <para>The tactic <command>elimType</command> </para>
- </sect2>
- <sect2 id="tac_exact">
- <title>exact <term></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 <reduction_kind> <term> <pattern></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 <ident> [<ident list>]</title>
- <para>The tactic <command>fwd</command> </para>
- </sect2>
- <sect2 id="tac_generalize">
- <title>generalize <pattern> [as <id>]</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 <term></title>
- <para>The tactic <command>injection</command> </para>
- </sect2>
- <sect2 id="tac_intro">
- <title>intro [<ident>]</title>
- <para>The tactic <command>intro</command> </para>
- </sect2>
- <sect2 id="tac_intros">
- <title>intros <intros_spec></title>
- <para>The tactic <command>intros</command> </para>
- </sect2>
- <sect2 id="tac_inversion">
- <title>intros <term></title>
- <para>The tactic <command>intros</command> </para>
- </sect2>
- <sect2 id="tac_lapply">
- <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</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 <ident> ≝ <term></title>
- <para>The tactic <command>letin</command> </para>
- </sect2>
- <sect2 id="tac_normalize">
- <title>normalize <pattern></title>
- <para>The tactic <command>normalize</command> </para>
- </sect2>
- <sect2 id="tac_paramodulation">
- <title>paramodulation <pattern></title>
- <para>The tactic <command>paramodulation</command> </para>
- </sect2>
- <sect2 id="tac_reduce">
- <title>reduce <pattern></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 <pattern> with <term></title>
- <para>The tactic <command>replace</command> </para>
- </sect2>
- <sect2 id="tac_rewrite">
- <title>rewrite {<|>} <term> <pattern></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 <pattern></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 <term></title>
- <para>The tactic <command>transitivity</command> </para>
- </sect2>
- <sect2 id="tac_unfold">
- <title>unfold [<term>] <pattern></title>
- <para>The tactic <command>unfold</command> </para>
- </sect2>
- <sect2 id="tac_whd">
- <title>whd <pattern></title>
- <para>The tactic <command>whd</command> </para>
- </sect2>
-
-</sect1>
+++ /dev/null
-
-<!-- =========== 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>
-
--- /dev/null
+@MATITA_VERSION@
projects / helm.git / commitdiff