From 9697aca10f3bf914764b099a5002a2c0e9c47e4d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Feb 2006 17:55:19 +0000 Subject: [PATCH] Even more tactics documented. --- matita/help/C/sec_tactics.xml | 149 ++++++++++++++++++++++++++++++++-- 1 file changed, 143 insertions(+), 6 deletions(-) diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index caee727a4..5844ffcea 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -860,22 +860,113 @@ its constructor takes no arguments. letin <ident> ≝ <term> letin - The tactic letin + letin x ≝ t + + + + Pre-conditions: + + none. + + + + Action: + + it adds to the context of the current sequent to prove a new + definition x ≝ t. + + + + New sequents to prove: + + none. + + + + normalize <pattern> normalize - The tactic normalize + normalize patt + + + + Pre-conditions: + + none. + + + + Action: + + it replaces all the terms matched by patt + with their βδιζ-normal form. + + + + New sequents to prove: + + none. + + + + paramodulation <pattern> paramodulation - The tactic paramodulation + paramodulation patt + + + + Pre-conditions: + + TODO. + + + + Action: + + TODO. + + + + New sequents to prove: + + TODO. + + + + reduce <pattern> reduce - The tactic reduce + reduce patt + + + + Pre-conditions: + + none. + + + + Action: + + it replaces all the terms matched by patt + with their βδιζ-normal form. + + + + New sequents to prove: + + none. + + + + reflexivity @@ -931,7 +1022,30 @@ its constructor takes no arguments. simplify <pattern> simplify - The tactic simplify + simplify patt + + + + Pre-conditions: + + none. + + + + Action: + + it replaces all the terms matched by patt + with other convertible terms that are supposed to be simpler. + + + + New sequents to prove: + + none. + + + + split @@ -956,7 +1070,30 @@ its constructor takes no arguments. whd <pattern> whd - The tactic whd + whd patt + + + + Pre-conditions: + + none. + + + + Action: + + it replaces all the terms matched by patt + with their βδιζ-weak-head normal form. + + + + New sequents to prove: + + none. + + + + -- 2.39.2