X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fmatita.xml;h=97b58e572a63c7cf8db2e720b3599adb0ccdb7ac;hb=740cea5493810e6e7e672d7791d2bc5cf62e656e;hp=1034d910b03c117a47271d16ab723b38afe5b837;hpb=d00ad097b410a4963657baa18280d57ed2082a03;p=helm.git diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index 1034d910b..97b58e572 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/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;