changeset 8265 | 187cada50e19 |
parent 8174 | 56d9baa2ddb0 |
child 8268 | 722074b93cdd |
8264:fffae6147cf7 | 8265:187cada50e19 |
---|---|
19 qed "IdE"; |
19 qed "IdE"; |
20 |
20 |
21 Goalw [Id_def] "(a,b):Id = (a=b)"; |
21 Goalw [Id_def] "(a,b):Id = (a=b)"; |
22 by (Blast_tac 1); |
22 by (Blast_tac 1); |
23 qed "pair_in_Id_conv"; |
23 qed "pair_in_Id_conv"; |
24 Addsimps [pair_in_Id_conv]; |
24 AddIffs [pair_in_Id_conv]; |
25 |
25 |
26 Goalw [refl_def] "reflexive Id"; |
26 Goalw [refl_def] "reflexive Id"; |
27 by Auto_tac; |
27 by Auto_tac; |
28 qed "reflexive_Id"; |
28 qed "reflexive_Id"; |
29 |
29 |