equal
deleted
inserted
replaced
295 qed |
295 qed |
296 |
296 |
297 |
297 |
298 subsection {* Type constructor for finite deflations *} |
298 subsection {* Type constructor for finite deflations *} |
299 |
299 |
300 defaultsort profinite |
300 default_sort profinite |
301 |
301 |
302 typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}" |
302 typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}" |
303 by (fast intro: finite_deflation_approx) |
303 by (fast intro: finite_deflation_approx) |
304 |
304 |
305 instantiation fin_defl :: (profinite) below |
305 instantiation fin_defl :: (profinite) below |