From bdb6fb19553a08101912c28ffb9c882393ccb11f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 6 Feb 2006 11:22:27 +0000 Subject: [PATCH] first sketch of the documentation (to be used by yelp) --- matita/help/C/legal.xml | 76 +++++++ matita/help/C/matita.xml | 432 +++++++++++++++++++++++++++++++++++++++ matita/matita.glade | 55 +++-- matita/matita.lang | 1 + matita/matitaGui.ml | 2 + 5 files changed, 549 insertions(+), 17 deletions(-) create mode 100644 matita/help/C/legal.xml create mode 100644 matita/help/C/matita.xml diff --git a/matita/help/C/legal.xml b/matita/help/C/legal.xml new file mode 100644 index 000000000..ac97e1de4 --- /dev/null +++ b/matita/help/C/legal.xml @@ -0,0 +1,76 @@ + + + Permission is granted to copy, distribute and/or modify this + document under the terms of the GNU Free Documentation + License (GFDL), Version 1.1 or any later version published + by the Free Software Foundation with no Invariant Sections, + no Front-Cover Texts, and no Back-Cover Texts. You can find + a copy of the GFDL at this link or in the file COPYING-DOCS + distributed with this manual. + + This manual is part of a collection of GNOME manuals + distributed under the GFDL. If you want to distribute this + manual separately from the collection, you can do so by + adding a copy of the license to the manual, as described in + section 6 of the license. + + + + Many of the names used by companies to distinguish their + products and services are claimed as trademarks. Where those + names appear in any GNOME documentation, and the members of + the GNOME Documentation Project are made aware of those + trademarks, then the names are in capital letters or initial + capital letters. + + + + DOCUMENT AND MODIFIED VERSIONS OF THE DOCUMENT ARE PROVIDED + UNDER THE TERMS OF THE GNU FREE DOCUMENTATION LICENSE + WITH THE FURTHER UNDERSTANDING THAT: + + + + DOCUMENT IS PROVIDED ON AN "AS IS" BASIS, + WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR + IMPLIED, INCLUDING, WITHOUT LIMITATION, WARRANTIES + THAT THE DOCUMENT OR MODIFIED VERSION OF THE + DOCUMENT IS FREE OF DEFECTS MERCHANTABLE, FIT FOR + A PARTICULAR PURPOSE OR NON-INFRINGING. THE ENTIRE + RISK AS TO THE QUALITY, ACCURACY, AND PERFORMANCE + OF THE DOCUMENT OR MODIFIED VERSION OF THE + DOCUMENT IS WITH YOU. SHOULD ANY DOCUMENT OR + MODIFIED VERSION PROVE DEFECTIVE IN ANY RESPECT, + YOU (NOT THE INITIAL WRITER, AUTHOR OR ANY + CONTRIBUTOR) ASSUME THE COST OF ANY NECESSARY + SERVICING, REPAIR OR CORRECTION. THIS DISCLAIMER + OF WARRANTY CONSTITUTES AN ESSENTIAL PART OF THIS + LICENSE. NO USE OF ANY DOCUMENT OR MODIFIED + VERSION OF THE DOCUMENT IS AUTHORIZED HEREUNDER + EXCEPT UNDER THIS DISCLAIMER; AND + + + + UNDER NO CIRCUMSTANCES AND UNDER NO LEGAL + THEORY, WHETHER IN TORT (INCLUDING NEGLIGENCE), + CONTRACT, OR OTHERWISE, SHALL THE AUTHOR, + INITIAL WRITER, ANY CONTRIBUTOR, OR ANY + DISTRIBUTOR OF THE DOCUMENT OR MODIFIED VERSION + OF THE DOCUMENT, OR ANY SUPPLIER OF ANY OF SUCH + PARTIES, BE LIABLE TO ANY PERSON FOR ANY + DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR + CONSEQUENTIAL DAMAGES OF ANY CHARACTER + INCLUDING, WITHOUT LIMITATION, DAMAGES FOR LOSS + OF GOODWILL, WORK STOPPAGE, COMPUTER FAILURE OR + MALFUNCTION, OR ANY AND ALL OTHER DAMAGES OR + LOSSES ARISING OUT OF OR RELATING TO USE OF THE + DOCUMENT AND MODIFIED VERSIONS OF THE DOCUMENT, + EVEN IF SUCH PARTY SHALL HAVE BEEN INFORMED OF + THE POSSIBILITY OF SUCH DAMAGES. + + + + + + diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml new file mode 100644 index 000000000..7f90e51b9 --- /dev/null +++ b/matita/help/C/matita.xml @@ -0,0 +1,432 @@ + + + + + + Matita"> + + +]> + + +
+ + + + &app; Manual V&manrevision; + + + 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 +
+ + +
+ + diff --git a/matita/matita.glade b/matita/matita.glade index 436dd7b26..71506d55a 100644 --- a/matita/matita.glade +++ b/matita/matita.glade @@ -877,7 +877,7 @@ - + True gtk-new 1 @@ -898,7 +898,7 @@ - + True gtk-open 1 @@ -919,7 +919,7 @@ - + True gtk-save 1 @@ -940,7 +940,7 @@ - + True gtk-save-as 1 @@ -961,7 +961,7 @@ - + True gtk-execute 1 @@ -988,7 +988,7 @@ - + True gtk-quit 1 @@ -1023,7 +1023,7 @@ - + True gtk-undo 1 @@ -1045,7 +1045,7 @@ - + True gtk-redo 1 @@ -1072,7 +1072,7 @@ - + True gtk-cut 1 @@ -1093,7 +1093,7 @@ - + True gtk-copy 1 @@ -1114,7 +1114,7 @@ - + True gtk-paste 1 @@ -1142,7 +1142,7 @@ True - + True gtk-delete 1 @@ -1183,7 +1183,7 @@ - + True gtk-find-and-replace 1 @@ -1352,7 +1352,7 @@ - + True gtk-zoom-in 1 @@ -1374,7 +1374,7 @@ - + True gtk-zoom-out 1 @@ -1395,7 +1395,7 @@ - + True gtk-zoom-100 1 @@ -1440,6 +1440,27 @@ + + + True + _Contents + True + + + + + True + gtk-help + 1 + 0.5 + 0.5 + 0 + 0 + + + + + True @@ -1447,7 +1468,7 @@ True - + True gtk-about 1 diff --git a/matita/matita.lang b/matita/matita.lang index 0c181ee44..d02231588 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -108,6 +108,7 @@ injection intro intros + inversion lapply left letin diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 34406a3cd..9cde82b75 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -206,6 +206,8 @@ class gui () = ~website:"http://helm.cs.unibo.it" () in + connect_menu_item main#contentsMenuItem + (fun () -> ignore (Sys.command "gnome-help ghelp:///home/claudio/miohelm/matita/help/C/matita.xml &")); connect_menu_item main#aboutMenuItem about_dialog#present; (* findRepl win *) let show_find_Repl () = -- 2.39.2