equal
deleted
inserted
replaced
99 apply (auto simp add: func_one func_times mult_ac) |
99 apply (auto simp add: func_one func_times mult_ac) |
100 done |
100 done |
101 |
101 |
102 instance "fun" :: (type,comm_ring_1)comm_ring_1 |
102 instance "fun" :: (type,comm_ring_1)comm_ring_1 |
103 apply default |
103 apply default |
104 apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def ext |
104 apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def |
105 func_one func_zero ring_simps) |
105 func_one func_zero algebra_simps) |
106 apply (drule fun_cong) |
106 apply (drule fun_cong) |
107 apply simp |
107 apply simp |
108 done |
108 done |
109 |
109 |
110 interpretation set_semigroup_add!: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set" |
110 interpretation set_semigroup_add!: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set" |