equal
deleted
inserted
replaced
78 shows "prod_fun id id \<equiv> id" |
78 shows "prod_fun id id \<equiv> id" |
79 by (rule eq_reflection) |
79 by (rule eq_reflection) |
80 (simp add: prod_fun_def) |
80 (simp add: prod_fun_def) |
81 |
81 |
82 lemma prod_rel_eq[id_simps]: |
82 lemma prod_rel_eq[id_simps]: |
83 shows "prod_rel op = op = \<equiv> op =" |
83 shows "prod_rel (op =) (op =) \<equiv> (op =)" |
84 apply (rule eq_reflection) |
84 apply (rule eq_reflection) |
85 apply (rule ext)+ |
85 apply (rule ext)+ |
86 apply auto |
86 apply auto |
87 done |
87 done |
88 |
88 |