X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_tactics.xml;h=c10d2bd337aabc49384f3c7984677369e751fce8;hb=54632bfcefb8f9cf2265b27196207b2786e84927;hp=2e1f6f36565e8a32f32c921e63badaf964e26a36;hpb=935a53fb77f36e5d90a2a59fa500744001e9d780;p=helm.git
diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index 2e1f6f365..c10d2bd33 100644
--- a/matita/help/C/sec_tactics.xml
+++ b/matita/help/C/sec_tactics.xml
@@ -750,7 +750,7 @@ its constructor takes no arguments.
fwd
fwd
- fwd ...TODO
+ fwd H
@@ -762,19 +762,29 @@ its constructor takes no arguments.
Pre-conditions:
- TODO.
+
+ The type of H must be the premise of a
+ forward simplification theorem.
+
Action:
- TODO.
+
+ This tactic is under development.
+ It simplifies the current context by removing
+ H using the following methods:
+ forward application of a suitable simplification theorem (chosen
+ automatically) of which the type of H is a
+ premise, decomposition, rewriting.
+
New sequents to prove:
- TODO.
+ None.
@@ -857,7 +867,7 @@ its constructor takes no arguments.
injection
- injection
+ injection
injection p