X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=cd26700ab703a885027108ae4bd5fa217dea8830;hb=5ad8f40e9fbad3c8f71c919d1a17a7201a4368eb;hp=e9f1567239ef53add4626f8705f6f3d37391d415;hpb=82794854730e383a5e388eeec0f89a77d1d2654c;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index e9f156723..cd26700ab 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -86,6 +86,59 @@
+
+ applyS
+ applyS
+ applyS t
+
+
+
+ Synopsis:
+
+ applyS &sterm;
+
+
+
+ Pre-conditions:
+
+ t must have type
+ T1 â ... â
+ Tn â G.
+
+
+
+ Action:
+
+ applyS is useful when
+ apply fails because the current goal
+ and the conclusion of the applied theorems are extensionally
+ equivalent up to instantiation of metavariables, but cannot
+ be unified. E.g. the goal is P(n*O+m) and
+ the theorem to be applied proves âm.P(m+O).
+
+
+ It tries to automatically rewrite the current goal using
+ auto paramodulation
+ to make it unifiable with G.
+ Then it closes the current sequent by applying
+ t to n
+ implicit arguments (that become new sequents).
+
+
+
+
+ New sequents to prove:
+
+ It opens a new sequent for each premise
+ Ti that is not
+ instantiated by unification. Ti is
+ the conclusion of the i-th new sequent to
+ prove.
+
+
+
+
+ assumptionassumption
@@ -1525,6 +1578,46 @@ its constructor takes no arguments.
+
+
+ subst
+ subst
+ subst
+
+
+
+ Synopsis:
+
+ subst
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ For each premise of the form
+ H: x = t or H: t = x
+ where x is a local variable and
+ t does not depend on x,
+ the tactic rewrites H wherever
+ x appears clearing H and
+ x afterwards.
+
+
+
+ New sequents to prove:
+
+ The one opened by the applied tactics.
+
+
+
+
+ symmetrysymmetry