From: Claudio Sacerdoti Coen Date: Fri, 13 Jul 2007 09:56:42 +0000 (+0000) Subject: Last crazy commit reverted. X-Git-Tag: make_still_working~6191 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c9cd5b62c814a9f3b90c2e1d96e4c4376af8f80f;p=helm.git Last crazy commit reverted. --- diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index 0b52d39e5..e20e17ad8 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -1,117 +1,178 @@ - -Enrico"> - Tassi"> - 21 Jun 2007"> - 1"> - gareuselesinge@debian.org"> - - matita"> - - - Debian"> - GNU"> - GPL"> + + + + + + + + + + + + + + + + + + + Matita"> + + + + TODO"> + MySQL "> + + + 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"> ]> - - -
- &dhemail; -
- - &dhfirstname; - &dhsurname; - + + + + + &app; V&appversion; User Manual (rev. &manrevision;) + + + - 2007 - &dhusername; + 2006 + The HELM team. - &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. - - - + + + Andrea + Asperti + +
asperti@cs.unibo.it
+ + + + Claudio + Sacerdoti Coen + +
sacerdot@cs.unibo.it
+ + + + Ferruccio + Guidi + +
fguidi@cs.unibo.it
+ + + + Enrico + Tassi + +
tassi@cs.unibo.it
+ + + + Stefano + Zacchiroli + +
zacchiro@cs.unibo.it
+ + + + + + 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; + + + + + + + +&intro; +&install; +&gettingstarted; +&terms; +&usernotation; +&tacticals; +&tactics; +&declarative_tactics; +&othercommands; +&license; + + + + diff --git a/helm/software/matita/help/C/tactics_quickref.xml b/helm/software/matita/help/C/tactics_quickref.xml index 119985dc4..e6f2e2f79 100644 --- a/helm/software/matita/help/C/tactics_quickref.xml +++ b/helm/software/matita/help/C/tactics_quickref.xml @@ -60,7 +60,7 @@ | - compose [&nat;] &sterm; [with &sterm;] [&intros-spec;] + compose [nat] sterm [with sterm] [intros-spec]