equal
deleted
inserted
replaced
299 by (rule lub_cprod2 [THEN thelubI]) |
299 by (rule lub_cprod2 [THEN thelubI]) |
300 |
300 |
301 lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y" |
301 lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y" |
302 by (simp add: csplit_def) |
302 by (simp add: csplit_def) |
303 |
303 |
304 lemma csplit3: "csplit\<cdot>cpair\<cdot>z = z" |
304 lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z" |
305 by (simp add: csplit_def surjective_pairing_Cprod2) |
305 by (simp add: csplit_def surjective_pairing_Cprod2) |
306 |
306 |
307 lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2 |
307 lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2 |
308 |
308 |
309 end |
309 end |