X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fmatita.xml;h=0b52d39e5a28dc3515da4f5679016cf62feb2179;hb=25b60c359f88d29e7f0b916c95cafc1cab06dc5b;hp=7f90e51b93536fc7f6c1e3d3cd3073008c060fc1;hpb=bdb6fb19553a08101912c28ffb9c882393ccb11f;p=helm.git diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml index 7f90e51b9..0b52d39e5 100644 --- a/matita/help/C/matita.xml +++ b/matita/help/C/matita.xml @@ -1,432 +1,117 @@ - - - - - - Matita"> - - + +Enrico"> + Tassi"> + 21 Jun 2007"> + 1"> + gareuselesinge@debian.org"> + + matita"> + + + Debian"> + GNU"> + GPL"> ]> - -
- - - - &app; Manual V&manrevision; + + +
+ &dhemail; +
+ + &dhfirstname; + &dhsurname; + + + 2007 + &dhusername; + + &dhdate; + + + &dhucpackage; + + &dhsection; + + + &dhpackage; + + creates XML data file for Vim7 omni completion from + DTDs + + + + &dhpackage; + filename.dtd + dialectname + + + + + DESCRIPTION + + This manual page documents brieftly the + &dhpackage; program. For more information see its HTML + documentation in + /usr/share/doc/vim-scripts/html/dtd2vim.html. + + + Starting from version 7 Vim supports context aware completion of XML + files (and others). In particular, when the file being edited is an XML + file, completion can be driven by the grammar extracted from a Document + Type Definition (DTD). + + For this feature to work the user should put an XML data file + corresponding to the desired DTD in a autoload/xml + directory contained in a directory belonging to Vim's + 'runtimepath' (for example + ~/.vim/autoload/xml/). + + &dhpackage; is the program that creates XML data + files from DTDs. Given as input a DTD + file.dtd it will create a + file.vim XML data file. + dialectname will be part of dictionary name + and will be used as argument for the :XMLns command. + + + + + + OPTIONS + + None. + + + + SEE ALSO + + vim (1). + + In the Vim online help: :help compl-omni, + :help ft-xml-omni, :help + :XMLns. + + dtd2vim is fully documented in + /usr/share/doc/vim-scripts/html/dtd2vim.html. + + + + + AUTHOR + + This manual page was written by &dhusername; &dhemail; for the + &debian; system (but may be used by others). Permission is granted to + copy, distribute and/or modify this document under the terms of the &gnu; + General Public License, Version 2 any later version published by the Free + Software Foundation. + + On Debian systems, the complete text of the GNU General Public + License can be found in /usr/share/common-licenses/GPL. + + + - - 2006 - The HELM team. - - - - - - &legal; - - - - - Andrea - Asperti - -
asperti@cs.unibo.it
- - - - Claudio - Sacerdoti Coen - -
sacerdot@cs.unibo.it
- - - - Enrico - Tassi - -
tassi@cs.unibo.it
- - - - Stefano - Zacchiroli - -
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. - - - - - - - - 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 -
- - -
- -