equal
deleted
inserted
replaced
179 apply(unfold rfun_def) |
179 apply(unfold rfun_def) |
180 apply(simp add: rfun'_Lam[OF f, OF c]) |
180 apply(simp add: rfun'_Lam[OF f, OF c]) |
181 apply(simp add: rfun_def) |
181 apply(simp add: rfun_def) |
182 done |
182 done |
183 |
183 |
|
184 |
184 end |
185 end |