From: Stefano Zacchiroli Date: Tue, 7 Feb 2006 13:39:52 +0000 (+0000) Subject: reshaped manual X-Git-Tag: 0.4.95@7852~1705 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8e20cf435e3ba53db9691e677b495816bf4d3047;p=helm.git reshaped manual --- diff --git a/configure.ac b/configure.ac index 15470ef37..afb09d805 100644 --- a/configure.ac +++ b/configure.ac @@ -154,19 +154,19 @@ AC_ARG_WITH(dbhost, AC_MSG_RESULT($DBHOST) AC_SUBST(CAMLP4O) -AC_SUBST(DISTRIBUTED) AC_SUBST(DBHOST) AC_SUBST(DEBUG) -AC_SUBST(TRANSFORMER_MODULE) -AC_SUBST(FINDLIB_REQUIRES) +AC_SUBST(DISTRIBUTED) AC_SUBST(FINDLIB_CREQUIRES) +AC_SUBST(FINDLIB_REQUIRES) AC_SUBST(HAVE_OCAMLOPT) AC_SUBST(LABLGLADECC) +AC_SUBST(MATITA_VERSION) AC_SUBST(OCAMLFIND) AC_SUBST(OCAMLPATH) AC_SUBST(RT_BASE_DIR) AC_SUBST(SRCROOT) -AC_SUBST(MATITA_VERSION) +AC_SUBST(TRANSFORMER_MODULE) AC_OUTPUT([ components/extlib/componentsConf.ml @@ -175,5 +175,6 @@ AC_OUTPUT([ matita/matita.conf.xml.build matita/buildTimeConf.ml matita/gtkmathview.matita.conf.xml + matita/dist/version.txt Makefile.defs ]) diff --git a/matita/dist/version.txt.in b/matita/dist/version.txt.in new file mode 100644 index 000000000..c275a8ce8 --- /dev/null +++ b/matita/dist/version.txt.in @@ -0,0 +1 @@ +@MATITA_VERSION@ diff --git a/matita/help/C/intro.xml b/matita/help/C/intro.xml new file mode 100644 index 000000000..5510c8eef --- /dev/null +++ b/matita/help/C/intro.xml @@ -0,0 +1,15 @@ + + + + + Introduction + + What is Matita? + + + Matita is a proof assistant for ... + + + + + diff --git a/matita/help/C/legal.xml b/matita/help/C/legal.xml index ac97e1de4..d457ff463 100644 --- a/matita/help/C/legal.xml +++ b/matita/help/C/legal.xml @@ -1,76 +1,19 @@ - - - Permission is granted to copy, distribute and/or modify this - document under the terms of the GNU Free Documentation - License (GFDL), Version 1.1 or any later version published - by the Free Software Foundation with no Invariant Sections, - no Front-Cover Texts, and no Back-Cover Texts. You can find - a copy of the GFDL at this link or in the file COPYING-DOCS - distributed with this manual. - - This manual is part of a collection of GNOME manuals - distributed under the GFDL. If you want to distribute this - manual separately from the collection, you can do so by - adding a copy of the license to the manual, as described in - section 6 of the license. - + This file is part of HELM, an Hypertextual, Electronic Library of + Mathematics, developed at the Computer Science Department, University of + Bologna, Italy. - - Many of the names used by companies to distinguish their - products and services are claimed as trademarks. Where those - names appear in any GNOME documentation, and the members of - the GNOME Documentation Project are made aware of those - trademarks, then the names are in capital letters or initial - capital letters. - + HELM is free software; you can redistribute it and/or modify it under + the terms of the GNU General Public License as published by the Free + Software Foundation; either version 2 of the License, or (at your option) + any later version. - - DOCUMENT AND MODIFIED VERSIONS OF THE DOCUMENT ARE PROVIDED - UNDER THE TERMS OF THE GNU FREE DOCUMENTATION LICENSE - WITH THE FURTHER UNDERSTANDING THAT: - - - - DOCUMENT IS PROVIDED ON AN "AS IS" BASIS, - WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR - IMPLIED, INCLUDING, WITHOUT LIMITATION, WARRANTIES - THAT THE DOCUMENT OR MODIFIED VERSION OF THE - DOCUMENT IS FREE OF DEFECTS MERCHANTABLE, FIT FOR - A PARTICULAR PURPOSE OR NON-INFRINGING. THE ENTIRE - RISK AS TO THE QUALITY, ACCURACY, AND PERFORMANCE - OF THE DOCUMENT OR MODIFIED VERSION OF THE - DOCUMENT IS WITH YOU. SHOULD ANY DOCUMENT OR - MODIFIED VERSION PROVE DEFECTIVE IN ANY RESPECT, - YOU (NOT THE INITIAL WRITER, AUTHOR OR ANY - CONTRIBUTOR) ASSUME THE COST OF ANY NECESSARY - SERVICING, REPAIR OR CORRECTION. THIS DISCLAIMER - OF WARRANTY CONSTITUTES AN ESSENTIAL PART OF THIS - LICENSE. NO USE OF ANY DOCUMENT OR MODIFIED - VERSION OF THE DOCUMENT IS AUTHORIZED HEREUNDER - EXCEPT UNDER THIS DISCLAIMER; AND - - - - UNDER NO CIRCUMSTANCES AND UNDER NO LEGAL - THEORY, WHETHER IN TORT (INCLUDING NEGLIGENCE), - CONTRACT, OR OTHERWISE, SHALL THE AUTHOR, - INITIAL WRITER, ANY CONTRIBUTOR, OR ANY - DISTRIBUTOR OF THE DOCUMENT OR MODIFIED VERSION - OF THE DOCUMENT, OR ANY SUPPLIER OF ANY OF SUCH - PARTIES, BE LIABLE TO ANY PERSON FOR ANY - DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR - CONSEQUENTIAL DAMAGES OF ANY CHARACTER - INCLUDING, WITHOUT LIMITATION, DAMAGES FOR LOSS - OF GOODWILL, WORK STOPPAGE, COMPUTER FAILURE OR - MALFUNCTION, OR ANY AND ALL OTHER DAMAGES OR - LOSSES ARISING OUT OF OR RELATING TO USE OF THE - DOCUMENT AND MODIFIED VERSIONS OF THE DOCUMENT, - EVEN IF SUCH PARTY SHALL HAVE BEEN INFORMED OF - THE POSSIBILITY OF SUCH DAMAGES. - - - - - + HELM is distributed in the hope that it will be useful, but WITHOUT + ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or + FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for + more details. + You should have received a copy of the GNU General Public License + along with HELM; if not, write to the Free Software Foundation, Inc., 59 + Temple Place - Suite 330, Boston, MA 02111-1307, USA. A copy of the GNU + General Public License is available at this link. diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml index 1034d910b..97b58e572 100644 --- a/matita/help/C/matita.xml +++ b/matita/help/C/matita.xml @@ -1,13 +1,17 @@ - - + + + + + + + Matita"> - + ]> @@ -15,7 +19,7 @@ - &app; Manual V&manrevision; + &app; V&appversion; Manual (rev. &manrevision;) 2006 @@ -38,10 +42,9 @@ --> - &legal; - + + &license; + @@ -88,7 +91,7 @@ - &appname; Manual V&manrevision; + &appname; V&appversion; Manual (rev. &manrevision;) &date; The HELM team @@ -120,10 +123,10 @@ section altogether --> Feedback - To report a bug or make a suggestion regarding the &app; application or - this manual, follow the directions in the - HELM Bugzilla Page. + To report a bug or make a suggestion regarding the &app; + application or this manual, follow the directions in the + HELM Bug + Tracking System Page. @@ -135,257 +138,16 @@ - - - Introduction - - What is Matita? - - - Matita is a proof assistant for ... - - - - - - - - Terms, definitions, declarations and proofs - - Terms - - - Definitions - - - Declarations (of inductive types) - - - Proofs - - - - - - Tactics - - - absurd <term> - The tactic absurd - -ciao - - - - 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 - - +&intro; +&terms; +&tactics; License - - This program is free software; you can redistribute it and/or - modify it under the terms of the GNU General Public - License as published by the Free Software Foundation; - either version 2 of the License, or (at your option) any later - version. - - - This program is distributed in the hope that it will be useful, but - WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - - A copy of the GNU General Public License is - included as an appendix to the GNOME Users - Guide. You may also obtain a copy of the - GNU General Public License from the Free - Software Foundation by visiting their Web site or by writing to -
- Free Software Foundation, Inc. - 59 Temple Place - Suite 330 - Boston, MA 02111-1307 - USA -
- + &license; diff --git a/matita/help/C/tactics.xml b/matita/help/C/tactics.xml new file mode 100644 index 000000000..a423f37c4 --- /dev/null +++ b/matita/help/C/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/matita/help/C/terms.xml b/matita/help/C/terms.xml new file mode 100644 index 000000000..d92518d8d --- /dev/null +++ b/matita/help/C/terms.xml @@ -0,0 +1,28 @@ + + + + + Terms, definitions, declarations and proofs + + + Terms + TODO + + + + Definitions + TODO + + + + Declarations (of inductive types) + TODO + + + + Proofs + TODO + + + +