From: Stefano Zacchiroli Date: Wed, 7 Jun 2006 14:50:33 +0000 (+0000) Subject: Attempt to make our markup respect the docbook specification(!), major changes X-Git-Tag: make_still_working~7255 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=871ed1c297e8c929a8c4460162e8521c9656bbc0;p=helm.git Attempt to make our markup respect the docbook specification(!), major changes required: 1) added wrappers where missing 2) added titles to tables 3) removed empty elements Point (3) make yelp now shows rules in tables used for syntax references. IMO this not a good reason to have empty elements, since they violates the docbook DTDs. Either yelp should be fixed to not ignore frame/rowsep/colsep attributes (as it currently does) or we need to find a different markup for displaying EBNF like grammars. --- diff --git a/helm/software/matita/help/C/sec_commands.xml b/helm/software/matita/help/C/sec_commands.xml index b1bada0fd..b4a6c8007 100644 --- a/helm/software/matita/help/C/sec_commands.xml +++ b/helm/software/matita/help/C/sec_commands.xml @@ -2,6 +2,11 @@ Other commands - &TODO; + + Introduction + + &TODO; + + diff --git a/helm/software/matita/help/C/sec_gettingstarted.xml b/helm/software/matita/help/C/sec_gettingstarted.xml index 886603ab2..5f9dda35a 100644 --- a/helm/software/matita/help/C/sec_gettingstarted.xml +++ b/helm/software/matita/help/C/sec_gettingstarted.xml @@ -11,22 +11,22 @@ How to type Unicode symbols - Unicode characters can be typed in several ways: + Unicode characters can be typed in several ways: - Using the "Shift+Ctrl+Unicode code" standard - Gnome shortcut. E.g. Shift+Ctrl+3a9 generates "Ω". + Using the "Shift+Ctrl+Unicode code" standard Gnome shortcut. E.g. Shift+Ctrl+3a9 generates "Ω". - Typing the ligature "\name" where "name" + Typing the ligature "\name" where "name" is a standard Unicode or LaTeX name for the character. Pressing "Alt+L" just after the last character of the name converts the ligature to the Unicode symbol. This operation is not required since Matita understands also the "\name" sequences. E.g. "\Omega" followed by Alt+L generates - "Ω". + "Ω". - Typing one of the following ligatures (and opzionally converting - the ligature to the Unicode character has described before): - ":=" (which stands for ≝); "->" (which stands for "→"); "=>" (which stands for "⇒"). + Typing one of the following ligatures (and optionally + converting the ligature to the Unicode character has described before): + ":=" (which stands for ≝); "->" (which stands for + "→"); "=>" (which stands for "⇒"). @@ -66,33 +66,32 @@ an action in the drop down menu right of it. Searching by name - &TODO; - + &TODO; + List of lemmas that can be applied - &TODO; - + &TODO; + Searching by exact match - &TODO; - + &TODO; + List of elimination principles for a given type - &TODO; - + &TODO; + Searching by instantiation - &TODO; - + &TODO; + Authoring How to use developments - &TODO; - - &TODO; - + &TODO; + + diff --git a/helm/software/matita/help/C/sec_intro.xml b/helm/software/matita/help/C/sec_intro.xml index a29b4960d..773bda24c 100644 --- a/helm/software/matita/help/C/sec_intro.xml +++ b/helm/software/matita/help/C/sec_intro.xml @@ -5,43 +5,44 @@ Introduction Features - - - Matita is an interactive theorem prover + Matita is an interactive theorem prover (or proof assistant) with the following characteristics: - - It is based on a variant of the Calculus of (co)Inductive - Constructions (CIC). CIC is also the logic of the Coq proof assistant. - - It adopts a procedural proof language, but it has a new - set of small step tacticals that improve proof structuring and debugging. - - It has a stand-alone graphical user interface (GUI) inspired by - CtCoq/Proof General. The GUI is implemented according to the state - of the art. In particular: - - It is based and fully integrated with Gtk/Gnome. - An on-line help can be browsed via the Gnome documentation - browser. - Mathematical formulae are rendered in two dimensional - notation via MathML and Unicode. - - - It integrates advanced browsing and searching procedures. - - It allows the use of the typical ambiguous mathematical notation - by means of a disambiguating parser. - - It is compatible with the library of Coq (definitions and - proof objects). - + + It is based on a variant of the Calculus of (co)Inductive Constructions (CIC). CIC is also the logic of the Coq proof assistant. + + + It adopts a procedural proof language, but it has a new set of small step tacticals that improve proof structuring and debugging. + + + It has a stand-alone graphical user interface (GUI) inspired by +CtCoq/Proof General. The GUI is implemented according to the state +of the art. In particular: + + + It is based and fully integrated with Gtk/Gnome. + + + An on-line help can be browsed via the Gnome documentation browser. + + + Mathematical formulae are rendered in two dimensional notation via MathML and Unicode. + + + + + It integrates advanced browsing and searching procedures. + + + It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser. + + + It is compatible with the library of Coq (definitions and proof objects). + - Matita vs Coq - The system shares a common look&feel with the Coq proof assistant and its graphical user interface. The two systems have the same logic, @@ -50,38 +51,46 @@ From the user point of view the main lacking features with respect to Coq are: - - proof extraction; - an extensible language of tactics; - automatic implicit arguments; - several ad-hoc decision procedures; - several rarely used variants for most of the tactics; - sections and local variables. To maintain compatibility - with the library of Coq, theorems defined inside sections are abstracted - by name over the section variables; their instances are explicitly - applied to actual arguments by means of explicit named - substitutions. + + proof extraction; + + + an extensible language of tactics; + + + automatic implicit arguments; + + + several ad-hoc decision procedures; + + + several rarely used variants for most of the tactics; + + + sections and local variables. To maintain compatibility with the library of Coq, theorems defined inside sections are abstracted by name over the section variables; their instances are explicitly applied to actual arguments by means of explicit named substitutions. + - Still from the user point of view, the main differences with respect to Coq are: - - the language of tacticals that allows execution of partial - tactical application; - the unification of the concept of metavariable and existential - variable; - terms with subterms that cannot be inferred are always allowed - as arguments of tactics or other commands; - ambiguous terms are disambiguated by direct interaction - with the user; - theorems and definitions in the library are always accessible - without needing to require/include them; right now, only notation needs - to be included to become active, but we plan to remove this limitation. + + the language of tacticals that allows execution of partial tactical application; + + + the unification of the concept of metavariable and existential variable; + + + terms with subterms that cannot be inferred are always allowed as arguments of tactics or other commands; + + + ambiguous terms are disambiguated by direct interaction with the user; + + + theorems and definitions in the library are always accessible without needing to require/include them; right now, only notation needs to be included to become active, but we plan to remove this limitation. + - diff --git a/helm/software/matita/help/C/sec_tacticals.xml b/helm/software/matita/help/C/sec_tacticals.xml index 870feed7c..ea863605f 100644 --- a/helm/software/matita/help/C/sec_tacticals.xml +++ b/helm/software/matita/help/C/sec_tacticals.xml @@ -2,6 +2,11 @@ Tacticals - &TODO; + + Introduction + + &TODO; + + diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 6d359a7ac..fbf8dd4ef 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -5,62 +5,67 @@ Syntax To describe syntax in this manual we use the following conventions: - Non terminal symbols are emphasized and have a link to their definition. E.g.: &term; - Terminal symbols are in bold. E.g.: theorem - Optional sequences of elements are put in square brackets. - E.g.: [in &term;] - Alternatives are put in square brakets and they are separated - by vertical bars. E.g.: [<|>] - Repetition of sequences of elements are given by putting the + Non terminal symbols are emphasized and have a link to their + definition. E.g.: &term; + Terminal symbols are in bold. E.g.: + theorem + Optional sequences of elements are put in square brackets. + E.g.: [in &term;] + Alternatives are put in square brakets and they are + separated by vertical bars. E.g.: [<|>] + Repetition of sequences of elements are given by putting the first sequence in square brackets, that are followed by three dots. - E.g.: [and &term;]… + E.g.: [and &term;]… Terms & co. Lexical conventions - - - - - - &id; - ::= - 〈〈&TODO;〉〉 - - - -
- - - - - - &nat; - ::= - 〈〈&TODO;〉〉 - - - -
- - - - - - &uri; - ::= - 〈〈&TODO;〉〉 - - - -
+ + + id + + + + &id; + ::= + 〈〈&TODO;〉〉 + + + +
+ + nat + + + + &nat; + ::= + 〈〈&TODO;〉〉 + + + +
+ + uri + + + + &uri; + ::= + 〈〈&TODO;〉〉 + + + +
+ Terms - + +
+ Terms - &term; @@ -144,9 +149,9 @@
- +
+ Simple terms - &sterm; @@ -241,9 +246,9 @@
- +
+ Arguments - &args; @@ -277,9 +282,9 @@
- +
+ Miscellaneous arguments - &args2; @@ -297,9 +302,9 @@
- +
+ Pattern matching - &match_pattern; @@ -316,6 +321,7 @@
+ diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml index 92698f824..dd1362d02 100644 --- a/helm/software/matita/help/C/sec_usernotation.xml +++ b/helm/software/matita/help/C/sec_usernotation.xml @@ -2,6 +2,11 @@ Extending the syntax - &TODO; + + Introduction + + &TODO; + +