changeset 31 | 04f43a28c97a |
parent 26 | 5e3aa998e94e |
--- a/prod.ML Wed Jan 05 19:39:05 1994 +0100 +++ b/prod.ML Fri Jan 07 14:22:37 1994 +0100 @@ -60,6 +60,12 @@ val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq]; +goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; +by(res_inst_tac[("p","s")]PairE 1); +by(res_inst_tac[("p","t")]PairE 1); +by(asm_simp_tac pair_ss 1); +val pair_eq = result(); + (*Prevents simplification of c: much faster*) val split_weak_cong = prove_goal Prod.thy "p=q ==> split(p,c) = split(q,c)"