equal
deleted
inserted
replaced
296 qed "surjective_pairing_Sprod"; |
296 qed "surjective_pairing_Sprod"; |
297 |
297 |
298 Goal "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"; |
298 Goal "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"; |
299 by (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1); |
299 by (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1); |
300 by (rotate_tac ~1 1); |
300 by (rotate_tac ~1 1); |
301 by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1); |
301 by (asm_lr_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1); |
302 by (Asm_simp_tac 1); |
302 by (Asm_simp_tac 1); |
303 qed "Sel_injective_Sprod"; |
303 qed "Sel_injective_Sprod"; |