X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Ftactic_quickref.xml;h=e44a53068e7bd6a17bcde0c95b23dca929c30e63;hb=f01ea391a615404b49aee832452bec33d3e595dd;hp=6a735eee247779b3bb19494190ebb2c3e556b92c;hpb=a094832a413d3d11cd4031b01a5119452384a7ac;p=helm.git diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml index 6a735eee2..e44a53068 100644 --- a/matita/help/C/tactic_quickref.xml +++ b/matita/help/C/tactic_quickref.xml @@ -1,186 +1,299 @@ - - - absurd sterm - - - apply sterm - - - - - assumption - - - - - auto [depth=nat] [width=nat] [paramodulation] [full] - - - change pattern with sterm - - - clear id - - - clearbody id - - - constructor nat - - - - - contradiction - - - - - cut sterm [as id] - - - + + tactics + + + + &tactic; + ::= + absurd sterm + + + + | + apply sterm + + + + | + applyS sterm + + + + | + + + assumption + + + + + + | + auto [depth=nat] [width=nat] [paramodulation] [full] + + + + | + change pattern with sterm + + + + | + + clear + id [id…] + + + + + | + clearbody id + + + + | + constructor nat + + + + | + + + contradiction + + + + + + | + cut sterm [as id] + + + + | + decompose - [([id]…)] - id intros-spec - - - - demodulation pattern - - - discriminate sterm - - - elim sterm [using sterm] intros-spec - - - elimType sterm [using sterm] intros-spec - - - exact sterm - - - - - exists - - - - - - - fail - - - - - fold reduction-kind sterm pattern - - - - - fourier - - - - - fwd id [as id [id]…] - - - generalize pattern [as id] - - - - - id - - - - - injection sterm - - - intro [id] - - - intros intros-spec - - - inversion sterm - - - lapply [depth=nat] sterm [to sterm [sterm]…] [as id] - - - - - left - - - - - letin id ≝ sterm - - - normalize pattern - - - paramodulation pattern - - - reduce pattern - - - - - reflexivity - - - - - replace pattern with sterm - - - rewrite [<|>] sterm pattern - - - - - right - - - - - - - ring - - - - - simplify pattern - - - - - split - - - - - - - symmetry - - - - - transitivity sterm - - - unfold [sterm] pattern - - - whd pattern - - + [( + id… + )] + [id] + [as id…] + + + + + | + + + demodulate + + + + + + | + discriminate sterm + + + + | + elim sterm [using sterm] intros-spec + + + + | + elimType sterm [using sterm] intros-spec + + + + | + exact sterm + + + + | + + + exists + + + + + + | + + + fail + + + + + + | + fold reduction-kind sterm pattern + + + + | + + + fourier + + + + + + | + fwd id [as id [id]…] + + + + | + generalize pattern [as id] + + + + | + + + id + + + + + + | + injection sterm + + + + | + intro [id] + + + + | + intros intros-spec + + + + | + inversion sterm + + + + | + + lapply + [linear] + [depth=nat] + sterm + [to + sterm + [,sterm…] + ] + [as id] + + + + + | + + + left + + + + + + | + letin id ≝ sterm + + + + | + normalize pattern + + + + | + reduce pattern + + + + | + + + reflexivity + + + + + + | + replace pattern with sterm + + + + | + rewrite [<|>] sterm pattern + + + + | + + + right + + + + + + | + + + ring + + + + + + | + simplify pattern + + + + | + + + split + + + + + + | + + + symmetry + + + + + + | + transitivity sterm + + + + | + unfold [sterm] pattern + + + + | + whd pattern + + + +