src/HOLCF/Lift.thy

--- a/src/HOLCF/Lift.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Lift.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -14,6 +14,9 @@
 pcpodef 'a lift = "UNIV :: 'a discr u set"
 by simp
 
+instance lift :: (finite) finite_po
+by (rule typedef_finite_po [OF type_definition_lift])
+
 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
 
 definition