| changeset 8226 | 07284f7ad262 |
| parent 8173 | a9966d5ab84d |
| child 8253 | 975eb12aa040 |
| 8225:fc5db20d7f6f | 8226:07284f7ad262 |
|---|---|
35 |
35 |
36 Goalw [id_def] "id x = x"; |
36 Goalw [id_def] "id x = x"; |
37 by (rtac refl 1); |
37 by (rtac refl 1); |
38 qed "id_apply"; |
38 qed "id_apply"; |
39 Addsimps [id_apply]; |
39 Addsimps [id_apply]; |
40 |
|
41 Goal "inv id = id"; |
|
42 by (simp_tac (simpset() addsimps [inv_def,id_def]) 1); |
|
43 qed "inv_id"; |
|
44 Addsimps [inv_id]; |
|
40 |
45 |
41 |
46 |
42 section "o"; |
47 section "o"; |
43 |
48 |
44 Goalw [o_def] "(f o g) x = f (g x)"; |
49 Goalw [o_def] "(f o g) x = f (g x)"; |