equal
deleted
inserted
replaced
29 \rulename{add_2_eq_Suc} |
29 \rulename{add_2_eq_Suc} |
30 |
30 |
31 @{thm[display] add_2_eq_Suc'[no_vars]} |
31 @{thm[display] add_2_eq_Suc'[no_vars]} |
32 \rulename{add_2_eq_Suc'} |
32 \rulename{add_2_eq_Suc'} |
33 |
33 |
34 @{thm[display] add_assoc[no_vars]} |
34 @{thm[display] add.assoc[no_vars]} |
35 \rulename{add_assoc} |
35 \rulename{add.assoc} |
36 |
36 |
37 @{thm[display] add_commute[no_vars]} |
37 @{thm[display] add.commute[no_vars]} |
38 \rulename{add_commute} |
38 \rulename{add.commute} |
39 |
39 |
40 @{thm[display] add_left_commute[no_vars]} |
40 @{thm[display] add.left_commute[no_vars]} |
41 \rulename{add_left_commute} |
41 \rulename{add.left_commute} |
42 |
42 |
43 these form add_ac; similarly there is mult_ac |
43 these form add_ac; similarly there is mult_ac |
44 *} |
44 *} |
45 |
45 |
46 lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)" |
46 lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)" |