]> matita.cs.unibo.it Git - helm.git/blob - matita/help/C/tactic_quickref.xml
- fwd concrete syntax fixed
[helm.git] / matita / help / C / tactic_quickref.xml
1 <itemizedlist>
2   <listitem>
3     <para><link linkend="tac_absurd"><emphasis role="bold">absurd</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
4   </listitem>
5   <listitem>
6     <para><link linkend="tac_apply"><emphasis role="bold">apply</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
7   </listitem>
8   <listitem>
9     <para>
10       <link linkend="tac_assumption">
11         <emphasis role="bold">assumption</emphasis>
12       </link>
13     </para>
14   </listitem>
15   <listitem>
16     <para><link linkend="tac_auto"><emphasis role="bold">auto</emphasis></link> [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bold">width=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] [<emphasis role="bold">paramodulation</emphasis>] [<emphasis role="bold">full</emphasis>]</para>
17   </listitem>
18   <listitem>
19     <para><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
20   </listitem>
21   <listitem>
22     <para><link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></para>
23   </listitem>
24   <listitem>
25     <para><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></para>
26   </listitem>
27   <listitem>
28     <para><link linkend="tac_constructor"><emphasis role="bold">constructor</emphasis></link> <emphasis><link linkend="grammar.nat">nat</link></emphasis></para>
29   </listitem>
30   <listitem>
31     <para>
32       <link linkend="tac_contradiction">
33         <emphasis role="bold">contradiction</emphasis>
34       </link>
35     </para>
36   </listitem>
37   <listitem>
38     <para><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
39   </listitem>
40   <listitem>
41     <para>
42              <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
43              [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
44              <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis>
45             </para>
46   </listitem>
47   <listitem>
48     <para><link linkend="tac_demodulation"><emphasis role="bold">demodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
49   </listitem>
50   <listitem>
51     <para><link linkend="tac_discriminate"><emphasis role="bold">discriminate</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
52   </listitem>
53   <listitem>
54     <para><link linkend="tac_elim"><emphasis role="bold">elim</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
55   </listitem>
56   <listitem>
57     <para><link linkend="tac_elimType"><emphasis role="bold">elimType</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">using</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
58   </listitem>
59   <listitem>
60     <para><link linkend="tac_exact"><emphasis role="bold">exact</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
61   </listitem>
62   <listitem>
63     <para>
64       <link linkend="tac_exists">
65         <emphasis role="bold">exists</emphasis>
66       </link>
67     </para>
68   </listitem>
69   <listitem>
70     <para>
71       <link linkend="tac_fail">
72         <emphasis role="bold">fail</emphasis>
73       </link>
74     </para>
75   </listitem>
76   <listitem>
77     <para><link linkend="tac_fold"><emphasis role="bold">fold</emphasis></link> <emphasis><link linkend="grammar.reduction-kind">reduction-kind</link></emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
78   </listitem>
79   <listitem>
80     <para>
81       <link linkend="tac_fourier">
82         <emphasis role="bold">fourier</emphasis>
83       </link>
84     </para>
85   </listitem>
86   <listitem>
87     <para><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]…]</para>
88   </listitem>
89   <listitem>
90     <para><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
91   </listitem>
92   <listitem>
93     <para>
94       <link linkend="tac_id">
95         <emphasis role="bold">id</emphasis>
96       </link>
97     </para>
98   </listitem>
99   <listitem>
100     <para><link linkend="tac_injection"><emphasis role="bold">injection</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
101   </listitem>
102   <listitem>
103     <para><link linkend="tac_intro"><emphasis role="bold">intro</emphasis></link> [<emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
104   </listitem>
105   <listitem>
106     <para><link linkend="tac_intros"><emphasis role="bold">intros</emphasis></link> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
107   </listitem>
108   <listitem>
109     <para><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
110   </listitem>
111   <listitem>
112     <para><link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link> [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">to</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>]…] [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
113   </listitem>
114   <listitem>
115     <para>
116       <link linkend="tac_left">
117         <emphasis role="bold">left</emphasis>
118       </link>
119     </para>
120   </listitem>
121   <listitem>
122     <para><link linkend="tac_letin"><emphasis role="bold">letin</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis role="bold">≝</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
123   </listitem>
124   <listitem>
125     <para><link linkend="tac_normalize"><emphasis role="bold">normalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
126   </listitem>
127   <listitem>
128     <para><link linkend="tac_paramodulation"><emphasis role="bold">paramodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
129   </listitem>
130   <listitem>
131     <para><link linkend="tac_reduce"><emphasis role="bold">reduce</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
132   </listitem>
133   <listitem>
134     <para>
135       <link linkend="tac_reflexivity">
136         <emphasis role="bold">reflexivity</emphasis>
137       </link>
138     </para>
139   </listitem>
140   <listitem>
141     <para><link linkend="tac_replace"><emphasis role="bold">replace</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
142   </listitem>
143   <listitem>
144     <para><link linkend="tac_rewrite"><emphasis role="bold">rewrite</emphasis></link> [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>] <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
145   </listitem>
146   <listitem>
147     <para>
148       <link linkend="tac_right">
149         <emphasis role="bold">right</emphasis>
150       </link>
151     </para>
152   </listitem>
153   <listitem>
154     <para>
155       <link linkend="tac_ring">
156         <emphasis role="bold">ring</emphasis>
157       </link>
158     </para>
159   </listitem>
160   <listitem>
161     <para><link linkend="tac_simplify"><emphasis role="bold">simplify</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
162   </listitem>
163   <listitem>
164     <para>
165       <link linkend="tac_split">
166         <emphasis role="bold">split</emphasis>
167       </link>
168     </para>
169   </listitem>
170   <listitem>
171     <para>
172       <link linkend="tac_symmetry">
173         <emphasis role="bold">symmetry</emphasis>
174       </link>
175     </para>
176   </listitem>
177   <listitem>
178     <para><link linkend="tac_transitivity"><emphasis role="bold">transitivity</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
179   </listitem>
180   <listitem>
181     <para><link linkend="tac_unfold"><emphasis role="bold">unfold</emphasis></link> [<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>] <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
182   </listitem>
183   <listitem>
184     <para><link linkend="tac_whd"><emphasis role="bold">whd</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
185   </listitem>
186 </itemizedlist>