1theory Util
2 imports Main
3begin
4
5lemma prod_split_asmE:
6 "\<lbrakk> (a,b) = x; P (fst x) (snd x) \<rbrakk> \<Longrightarrow> P a b"
7 by (clarsimp split: prod.split)
8
9lemma prod_eq:
10 "\<lbrakk> a = fst x ; b = snd x \<rbrakk> \<Longrightarrow> x = (a,b)"
11 by simp
12
13end