| changeset 81584 | a065d8bcfd3d |
| parent 81583 | b6df83045178 |
| child 81644 | 325593146d19 |
--- a/src/HOL/HOLCF/Algebraic.thy Thu Dec 12 15:45:29 2024 +0100 +++ b/src/HOL/HOLCF/Algebraic.thy Thu Dec 12 16:57:06 2024 +0100 @@ -24,7 +24,7 @@ instance fin_defl :: (bifinite) po using type_definition_fin_defl below_fin_defl_def -by (rule typedef_po) +by (rule typedef_po_class) lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)" using Rep_fin_defl by simp