X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Ftactic_quickref.xml;h=dd14d8a2685b15d99c9493b9bebeaf21a7de122a;hb=48aa99d1d9659e55d68ab3ef50b10bc6165eee03;hp=e1f7eb434e1c530e1bef0f22fc0a38e1356bd10a;hpb=522d835109b6df16e1c082ae128c0e08677cbb1b;p=helm.git
diff --git a/helm/software/matita/help/C/tactic_quickref.xml b/helm/software/matita/help/C/tactic_quickref.xml
index e1f7eb434..dd14d8a26 100644
--- a/helm/software/matita/help/C/tactic_quickref.xml
+++ b/helm/software/matita/help/C/tactic_quickref.xml
@@ -19,7 +19,10 @@
change pattern with sterm
- clear id
+
+ clear
+ id [idâ¦]
+
clearbody id
@@ -38,7 +41,14 @@
cut sterm [as id]
- decompose id [id]⦠intros-spec
+
+ decompose
+ [(
+ idâ¦
+ )]
+ [id]
+ [as idâ¦]
+
demodulation pattern
@@ -80,7 +90,7 @@
- fwd id [([id]â¦)]
+ fwd id [as id [id]â¦]
generalize pattern [as id]
@@ -105,7 +115,17 @@
inversion sterm
- lapply [depth=nat] sterm [to sterm [sterm]â¦] [as id]
+
+ lapply
+ [linear]
+ [depth=nat]
+ sterm
+ [to
+ sterm
+ [,stermâ¦]
+ ]
+ [as id]
+