| changeset 1552 | 6f71b5d46700 |
| parent 1465 | 5d7a7e439cec |
| child 1605 | 248e1e125ca0 |
| 1551:4a617e14d12c | 1552:6f71b5d46700 |
|---|---|
25 by (etac exE 1); |
25 by (etac exE 1); |
26 by (eresolve_tac prems 1); |
26 by (eresolve_tac prems 1); |
27 qed "idE"; |
27 qed "idE"; |
28 |
28 |
29 goalw Relation.thy [id_def] "(a,b):id = (a=b)"; |
29 goalw Relation.thy [id_def] "(a,b):id = (a=b)"; |
30 by(fast_tac prod_cs 1); |
30 by (fast_tac prod_cs 1); |
31 qed "pair_in_id_conv"; |
31 qed "pair_in_id_conv"; |
32 |
32 |
33 |
33 |
34 (** Composition of two relations **) |
34 (** Composition of two relations **) |
35 |
35 |