From dd91d9b3909b0f6bfd4c1de701620f46976e61bd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Feb 2006 14:27:37 +0000 Subject: [PATCH] More tactics documented. --- helm/software/matita/help/C/sec_tactics.xml | 80 ++++++++++++++++++++- 1 file changed, 77 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index 2c1afb0cf..9ba73d991 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -497,15 +497,89 @@ its constructor takes no arguments. fold <reduction_kind> <term> <pattern> - The tactic fold + fold red t patt + + + + Pre-conditions: + + the pattern must not specify the wanted term. + + + + Action: + + first of all it locates all the subterms matched by + patt. In the context of each matched subterm + it disambiguates the term t and reduces it + to its red normal form; then it replaces with + t every occurrence of the normal form in the + matched subterm. + + + + New sequents to prove: + + none. + + + + fourier - The tactic fourier + fourier + + + + Pre-conditions: + + the conclusion of the current sequent must be a linear + inequation over real numbers taken from standard library of + Coq. Moreover the inequations in the hypotheses must imply the + inequation in the conclusion of the current sequent. + + + + Action: + + it closes the current sequent by applying the Fourier method. + + + + New sequents to prove: + + none. + + + + fwd <ident> [<ident list>] - The tactic fwd + fwd ...TODO + + + + Pre-conditions: + + TODO. + + + + Action: + + TODO. + + + + New sequents to prove: + + TODO. + + + + generalize <pattern> [as <id>] -- 2.39.2