| changeset 16 | a92c10af61bd |
| parent 15 | bdabf71fa35b |
| child 17 | a5427713eef4 |
| 15:bdabf71fa35b | 16:a92c10af61bd |
|---|---|
48 apply(auto) |
48 apply(auto) |
49 done |
49 done |
50 |
50 |
51 value "add 2 3" |
51 value "add 2 3" |
52 |
52 |
53 (**commutative-associative**) |
|
53 lemma add_04: "add m (add n k) = add k (add m n)" |
54 lemma add_04: "add m (add n k) = add k (add m n)" |
54 apply(induct) |
55 apply(induct) |
55 apply(auto) |
56 apply(auto) |
56 oops |
57 oops |
57 |
58 |