equal
deleted
inserted
replaced
198 by (simp add: ssplit_def) |
198 by (simp add: ssplit_def) |
199 |
199 |
200 lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:)= f\<cdot>x\<cdot>y" |
200 lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:)= f\<cdot>x\<cdot>y" |
201 by (simp add: ssplit_def) |
201 by (simp add: ssplit_def) |
202 |
202 |
203 lemma ssplit3: "ssplit\<cdot>spair\<cdot>z = z" |
203 lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z" |
204 by (rule_tac p=z in sprodE, simp_all) |
204 by (rule_tac p=z in sprodE, simp_all) |
205 |
205 |
206 end |
206 end |