| changeset 3371 | 80f0d0b2f404 |
| parent 3023 | 01364e2f30ad |
| child 4059 | 59c1422c9da5 |
| 3370:5c5fdce3a4e4 | 3371:80f0d0b2f404 |
|---|---|
4 Copyright 1996 TU Muenchen |
4 Copyright 1996 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 open RelPow; |
7 open RelPow; |
8 |
8 |
9 goal RelPow.thy "R^1 = R"; |
9 goal RelPow.thy "!!R:: ('a*'a)set. R^1 = R"; |
10 by (Simp_tac 1); |
10 by (Simp_tac 1); |
11 qed "rel_pow_1"; |
11 qed "rel_pow_1"; |
12 Addsimps [rel_pow_1]; |
12 Addsimps [rel_pow_1]; |
13 |
13 |
14 goal RelPow.thy "(x,x) : R^0"; |
14 goal RelPow.thy "(x,x) : R^0"; |