| changeset 49834 | b27bbb021df1 |
| parent 45694 | 4a8743618257 |
| child 51489 | f738e6dbd844 |
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Fri Oct 12 15:08:29 2012 +0200 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy Fri Oct 12 18:58:20 2012 +0200 @@ -42,7 +42,7 @@ definition "UP = {f :: nat => 'a::zero. EX n. bound n f}" -typedef (open) 'a up = "UP :: (nat => 'a::zero) set" +typedef 'a up = "UP :: (nat => 'a::zero) set" morphisms Rep_UP Abs_UP proof - have "bound 0 (\<lambda>_. 0::'a)" by (rule boundI) (rule refl)