X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fmatita.xml;h=a24b969eb7af1efab225e30f89b0e0d834f2163d;hb=3802156c428a73566ba757d7ec97ecc60697a2d6;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..a24b969eb 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -1,47 +1,87 @@ - - - - + + + + + + + + + + + + + + + + Matita"> - + + + TODO"> + MySQL "> + Sqlite "> + + + id"> + uri"> + char"> + uri-step"> + nat"> + term"> + rec_def"> + match_pattern"> + match_branch"> + args"> + args2"> + sterm"> + intros-spec"> + pattern"> + reduction-kind"> + path"> + proof-script"> + proof-step"> + tactic"> + LCF-tactical"> + qstring"> + interpretation"> + auto_params"> + justification"> + simple_auto_param"> + interpretation_argument"> + interpretation_rhs"> + csymbol"> + usage"> + notation_lhs"> + layout"> + literal"> + notation_rhs"> + associativity"> + symbol"> + level2_meta"> + unparsed_ast"> + unparsed_meta"> ]> - -
- - - - &app; Manual V&manrevision; + - - 2006 - The HELM team. - - - - + - &legal; - + + 2006 + The HELM team. + @@ -58,6 +98,13 @@
sacerdot@cs.unibo.it
+ + Ferruccio + Guidi + +
fguidi@cs.unibo.it
+ + Enrico Tassi @@ -71,323 +118,39 @@
zacchiro@cs.unibo.it
- - + - - - - &appname; Manual V&manrevision; - &date; - - The HELM team - - - - - - - 0.0 - 4 February 2006 - HELM - - First draft completed. - - - - - This manual describes version &appversion; of &appname;. - - - - Feedback - To report a bug or make a suggestion regarding the &app; application or - this manual, follow the directions in the - HELM Bugzilla Page. - - + + Both &appname; and this document are free software, you can + redistribute them and/or modify them under the terms of the GNU General + Public License as published by the Free Software Foundation. See for more information. - + + + &manrevision; + &date; + + - - Matita - + - - - 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 - - - - - - - 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 -
- - -
+&intro; +&install; +&gettingstarted; +&terms; +&usernotation; +&tacticals; +&tactics; +&declarative_tactics; +&othercommands; +&license; + +