]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_tactics/README
several dialog boxes no longer used removed
[helm.git] / matita / components / ng_tactics / README
1 +letin: basta la refine fatta con occurcheck
2 +cut:   letin; clearbody ~-1 (cosa sia ~-1 รจ da capirsi)
3
4 -generalize:
5   a) verificare che tutti i termini selezionati siano convertibili
6   b) spostare i termini selezionati nel contesto corrente/spostare il
7      termine bucato sotto un lambda
8   c) bucare e liftare deve essere fatto contemporaneamente
9   d) poi usare tatticali per fare cut + apply
10
11 =fail:
12 =id:
13
14 apply:
15 applyS:
16 intros:
17 elim:
18 cases:
19 rewrite:
20 ??replace: rewrite (?:A=B); [2: apply eq_a_b ] 
21 =auto/demodulate/solve_rewrite:
22 change:
23 clear/clearbody:
24 destruct:
25 inversion:
26 lapply:
27 ??compose:
28 whd/simpl/normalize:
29 fold:
30 unfold:
31
32 assumption:
33 constructor:
34 exists:
35 left:
36 right:
37 reflexivity:
38 symmetry:
39 transitivity:
40 split:
41
42 decompose:
43
44 #####
45 absurd:
46 contradiction:
47 exact:
48 elim_type:
49 fourier:
50 ring:
51
52 ####
53 applyP:
54 fwd_simpl: