From 6073f0bd6760d393f229d1b61a91bf9b64af2f09 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Feb 2006 16:36:39 +0000 Subject: [PATCH] From article to book --- helm/software/matita/help/C/matita.xml | 36 ++-- helm/software/matita/help/C/sec_install.xml | 20 +-- helm/software/matita/help/C/sec_intro.xml | 8 +- helm/software/matita/help/C/sec_tactics.xml | 182 ++++++++++---------- helm/software/matita/help/C/sec_terms.xml | 20 +-- 5 files changed, 132 insertions(+), 134 deletions(-) diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index 45e993b05..0b27e59fb 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -1,6 +1,6 @@ - @@ -17,12 +17,13 @@ TODO"> ]> - -
+ + + - - &app; V&appversion; Manual (rev. &manrevision;) +&app; V&appversion; Manual (rev. &manrevision;) + 2006 @@ -45,10 +46,6 @@ --> - - &license; - - Andrea @@ -108,7 +105,7 @@ - 0.0 + &manrevision; 4 February 2006 HELM @@ -120,6 +117,11 @@ This manual describes version &appversion; of &appname;. + + + &license; + + - - - - Matita - + @@ -149,11 +147,11 @@ - + License &license; - -
+ + - + Installation - + Installing &appname; from sources Currently, the only intended way to install &appname; is starting from its source code. - + Getting the source code You can get the &appname; source code in two ways: @@ -38,9 +38,9 @@ - + - + Requirements In order to build &appname; from sources you will need some @@ -227,9 +227,9 @@ - + - + Instructions Once you get the source code the installations steps should be @@ -294,8 +294,8 @@ - + - - + + diff --git a/helm/software/matita/help/C/sec_intro.xml b/helm/software/matita/help/C/sec_intro.xml index 5510c8eef..a3dbc5166 100644 --- a/helm/software/matita/help/C/sec_intro.xml +++ b/helm/software/matita/help/C/sec_intro.xml @@ -1,15 +1,15 @@ - + Introduction - + What is Matita? Matita is a proof assistant for ... - - + + diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index 9ba73d991..7289130d9 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -1,19 +1,19 @@ - + Tactics - + absurd <term> absurd P - + + Pre-conditions: P must have type Prop. - Action: @@ -29,9 +29,9 @@ - - - + + + apply <term> apply t @@ -64,8 +64,8 @@ - - + + assumption assumption @@ -91,8 +91,8 @@ - - + + auto [depth=<int>] [width=<int>] [paramodulation] [full] auto depth=d width=w paramodulation full @@ -124,8 +124,8 @@ - - + + clear <id> clear H @@ -152,8 +152,8 @@ - - + + clearbody <id> clearbody H @@ -180,8 +180,8 @@ - - + + change <pattern> with <term> change patt with t @@ -211,8 +211,8 @@ - - + + constructor <int> constructor n @@ -241,8 +241,8 @@ - - + + contradiction contradiction @@ -269,8 +269,8 @@ - - + + cut <term> [as <id>] cut P as H @@ -299,8 +299,8 @@ - - + + decompose [<ident list>] <ident> [<intros_spec>] decompose ??? @@ -325,8 +325,8 @@ - - + + discriminate <term> discriminate p @@ -353,8 +353,8 @@ its constructor takes no arguments. - - + + elim <term> [using <term>] [<intros_spec>] elim t using th hyps @@ -386,8 +386,8 @@ its constructor takes no arguments. - - + + elimType <term> [using <term>] elimType T using th @@ -412,8 +412,8 @@ its constructor takes no arguments. - - + + exact <term> exact p @@ -439,8 +439,8 @@ its constructor takes no arguments. - - + + exists exists @@ -468,8 +468,8 @@ its constructor takes no arguments. - - + + fail fail @@ -494,8 +494,8 @@ its constructor takes no arguments. - - + + fold <reduction_kind> <term> <pattern> fold red t patt @@ -525,8 +525,8 @@ its constructor takes no arguments. - - + + fourier fourier @@ -554,8 +554,8 @@ its constructor takes no arguments. - - + + fwd <ident> [<ident list>] fwd ...TODO @@ -580,99 +580,99 @@ its constructor takes no arguments. - - + + 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 - + - + diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 4499f2344..70da94404 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -1,28 +1,28 @@ - + Terms, definitions, declarations and proofs - + Terms &TODO; - + - + Definitions &TODO; - + - + Declarations (of inductive types) &TODO; - + - + Proofs &TODO; - + - + -- 2.39.2