From: Stefano Zacchiroli Date: Tue, 7 Feb 2006 14:54:25 +0000 (+0000) Subject: - moved version.txt.in to the help dir X-Git-Tag: make_still_working~7607 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1da3c8d481853c3d6b9f33385ebde848866a37b5;p=helm.git - moved version.txt.in to the help dir - added Makefile to generate xhtml and pdf from the docbook manual --- diff --git a/helm/software/matita/dist/version.txt.in b/helm/software/matita/dist/version.txt.in deleted file mode 100644 index c275a8ce8..000000000 --- a/helm/software/matita/dist/version.txt.in +++ /dev/null @@ -1 +0,0 @@ -@MATITA_VERSION@ diff --git a/helm/software/matita/help/C/Makefile b/helm/software/matita/help/C/Makefile new file mode 100644 index 000000000..ad3ad6433 --- /dev/null +++ b/helm/software/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/helm/software/matita/help/C/intro.xml b/helm/software/matita/help/C/intro.xml deleted file mode 100644 index 5510c8eef..000000000 --- a/helm/software/matita/help/C/intro.xml +++ /dev/null @@ -1,15 +0,0 @@ - - - - - Introduction - - What is Matita? - - - Matita is a proof assistant for ... - - - - - diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index 97b58e572..a0da700e4 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -3,15 +3,16 @@ "http://www.oasis-open.org/docbook/xml/4.1.2/docbookx.dtd" [ - - - + + + + Matita"> - + ]> @@ -140,6 +141,7 @@ &intro; +&install; &terms; &tactics; diff --git a/helm/software/matita/help/C/sec_install.xml b/helm/software/matita/help/C/sec_install.xml new file mode 100644 index 000000000..308bf02fa --- /dev/null +++ b/helm/software/matita/help/C/sec_install.xml @@ -0,0 +1,27 @@ + + + + + Installation + + + Installing &appname; from sources + + Currently, the only intended way to install &appname; is starting + from its source code. + + + Getting the source code + + You can get the &appname; source code in two ways: + + foo + bar + + + + + + + + diff --git a/helm/software/matita/help/C/sec_intro.xml b/helm/software/matita/help/C/sec_intro.xml new file mode 100644 index 000000000..5510c8eef --- /dev/null +++ b/helm/software/matita/help/C/sec_intro.xml @@ -0,0 +1,15 @@ + + + + + Introduction + + What is Matita? + + + Matita is a proof assistant for ... + + + + + diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml new file mode 100644 index 000000000..a423f37c4 --- /dev/null +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -0,0 +1,189 @@ + + + + Tactics + + + absurd <term> + The tactic absurd + + + + + apply <term> + The tactic apply + + + assumption + The tactic assumption + + + auto [depth=<int>] [width=<int>] [paramodulation] [full] + The tactic auto + + + clear <id> + The tactic clear + + + clearbody <id> + The tactic clearbody + + + change <pattern> with <term> + The tactic change + + + compare <term> + The tactic compare + + + constructor <int> + The tactic constructor + + + contradiction + The tactic contradiction + + + cut <term> [as <id>] + The tactic cut + + + decide + The tactic decide equality + + + decompose [<ident list>] <ident> [<intros_spec>] + The tactic decompose + + + discriminate <term> + The tactic discriminate + + + elim <term> [using <term>] [<intros_spec>] + The tactic elim + + + elimType <term> [using <term>] + The tactic elimType + + + exact <term> + The tactic exact + + + exists + The tactic exists + + + fail + The tactic fail + + + fold <reduction_kind> <term> <pattern> + The tactic fold + + + fourier + The tactic fourier + + + fwd <ident> [<ident list>] + The tactic fwd + + + generalize <pattern> [as <id>] + The tactic generalize + + + id + The tactic id + + + injection <term> + The tactic injection + + + intro [<ident>] + The tactic intro + + + intros <intros_spec> + The tactic intros + + + intros <term> + The tactic intros + + + lapply [depth=<int>] <term> [to <term list] [using <ident>] + The tactic lapply + + + left + The tactic left + + + letin <ident> ≝ <term> + The tactic letin + + + normalize <pattern> + The tactic normalize + + + paramodulation <pattern> + The tactic paramodulation + + + reduce <pattern> + The tactic reduce + + + reflexivity + The tactic reflexivity + + + replace <pattern> with <term> + The tactic replace + + + rewrite {<|>} <term> <pattern> + The tactic rewrite + + + right + The tactic right + + + ring + The tactic ring + + + simplify <pattern> + The tactic simplify + + + split + The tactic split + + + symmetry + The tactic symmetry + + + transitivity <term> + The tactic transitivity + + + unfold [<term>] <pattern> + The tactic unfold + + + whd <pattern> + The tactic whd + + + diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml new file mode 100644 index 000000000..d92518d8d --- /dev/null +++ b/helm/software/matita/help/C/sec_terms.xml @@ -0,0 +1,28 @@ + + + + + Terms, definitions, declarations and proofs + + + Terms + TODO + + + + Definitions + TODO + + + + Declarations (of inductive types) + TODO + + + + Proofs + TODO + + + + diff --git a/helm/software/matita/help/C/tactics.xml b/helm/software/matita/help/C/tactics.xml deleted file mode 100644 index a423f37c4..000000000 --- a/helm/software/matita/help/C/tactics.xml +++ /dev/null @@ -1,189 +0,0 @@ - - - - Tactics - - - absurd <term> - The tactic absurd - - - - - apply <term> - The tactic apply - - - assumption - The tactic assumption - - - auto [depth=<int>] [width=<int>] [paramodulation] [full] - The tactic auto - - - clear <id> - The tactic clear - - - clearbody <id> - The tactic clearbody - - - change <pattern> with <term> - The tactic change - - - compare <term> - The tactic compare - - - constructor <int> - The tactic constructor - - - contradiction - The tactic contradiction - - - cut <term> [as <id>] - The tactic cut - - - decide - The tactic decide equality - - - decompose [<ident list>] <ident> [<intros_spec>] - The tactic decompose - - - discriminate <term> - The tactic discriminate - - - elim <term> [using <term>] [<intros_spec>] - The tactic elim - - - elimType <term> [using <term>] - The tactic elimType - - - exact <term> - The tactic exact - - - exists - The tactic exists - - - fail - The tactic fail - - - fold <reduction_kind> <term> <pattern> - The tactic fold - - - fourier - The tactic fourier - - - fwd <ident> [<ident list>] - The tactic fwd - - - generalize <pattern> [as <id>] - The tactic generalize - - - id - The tactic id - - - injection <term> - The tactic injection - - - intro [<ident>] - The tactic intro - - - intros <intros_spec> - The tactic intros - - - intros <term> - The tactic intros - - - lapply [depth=<int>] <term> [to <term list] [using <ident>] - The tactic lapply - - - left - The tactic left - - - letin <ident> ≝ <term> - The tactic letin - - - normalize <pattern> - The tactic normalize - - - paramodulation <pattern> - The tactic paramodulation - - - reduce <pattern> - The tactic reduce - - - reflexivity - The tactic reflexivity - - - replace <pattern> with <term> - The tactic replace - - - rewrite {<|>} <term> <pattern> - The tactic rewrite - - - right - The tactic right - - - ring - The tactic ring - - - simplify <pattern> - The tactic simplify - - - split - The tactic split - - - symmetry - The tactic symmetry - - - transitivity <term> - The tactic transitivity - - - unfold [<term>] <pattern> - The tactic unfold - - - whd <pattern> - The tactic whd - - - diff --git a/helm/software/matita/help/C/terms.xml b/helm/software/matita/help/C/terms.xml deleted file mode 100644 index d92518d8d..000000000 --- a/helm/software/matita/help/C/terms.xml +++ /dev/null @@ -1,28 +0,0 @@ - - - - - Terms, definitions, declarations and proofs - - - Terms - TODO - - - - Definitions - TODO - - - - Declarations (of inductive types) - TODO - - - - Proofs - TODO - - - - diff --git a/helm/software/matita/help/C/version.txt.in b/helm/software/matita/help/C/version.txt.in new file mode 100644 index 000000000..c275a8ce8 --- /dev/null +++ b/helm/software/matita/help/C/version.txt.in @@ -0,0 +1 @@ +@MATITA_VERSION@