| changeset 29063 | 7619f0561cd7 |
| parent 27311 | aa28b1d33866 |
| child 29138 | 661a8db7e647 |
--- a/src/HOLCF/Lift.thy Thu Dec 11 16:30:35 2008 +0100 +++ b/src/HOLCF/Lift.thy Thu Dec 11 16:50:18 2008 +0100 @@ -12,7 +12,7 @@ defaultsort type pcpodef 'a lift = "UNIV :: 'a discr u set" -by simp +by simp_all instance lift :: (finite) finite_po by (rule typedef_finite_po [OF type_definition_lift])