X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fmatita.xml;h=f66e6409336fd7698ed8d88f3acd3217e7f690c7;hb=57003fb8f7c54191f61585b9b7f067c3aab666e4;hp=0b52d39e5a28dc3515da4f5679016cf62feb2179;hpb=111df95ac03f2ee21dfa2422a7f531f675b1c16d;p=helm.git
diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index 0b52d39e5..f66e64093 100644
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -1,117 +1,196 @@
-
-Enrico">
- Tassi">
- 21 Jun 2007">
- 1">
- gareuselesinge@debian.org">
-
- matita">
-
-
- Debian">
- GNU">
- GPL">
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 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">
+ enriched_term">
]>
-
-
-
- &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;
+
+
+
+