equal
deleted
inserted
replaced
80 goal Prod.thy "(!x. P x) = (!a b. P(a,b))"; |
80 goal Prod.thy "(!x. P x) = (!a b. P(a,b))"; |
81 by(fast_tac (HOL_cs addbefore split_all_tac 1) 1); |
81 by(fast_tac (HOL_cs addbefore split_all_tac 1) 1); |
82 qed "split_paired_All"; |
82 qed "split_paired_All"; |
83 |
83 |
84 goalw Prod.thy [split_def] "split c (a,b) = c a b"; |
84 goalw Prod.thy [split_def] "split c (a,b) = c a b"; |
85 by (sstac [fst_conv, snd_conv] 1); |
85 by (EVERY1[stac fst_conv, stac snd_conv]); |
86 by (rtac refl 1); |
86 by (rtac refl 1); |
87 qed "split"; |
87 qed "split"; |
88 |
88 |
89 Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq]; |
89 Addsimps [fst_conv, snd_conv, split_paired_All, split, Pair_eq]; |
90 |
90 |