| changeset 49834 | b27bbb021df1 |
| parent 47252 | 3a096e7a1871 |
| child 53196 | 942a1b48bb31 |
--- a/src/HOL/Library/Fraction_Field.thy Fri Oct 12 15:08:29 2012 +0200 +++ b/src/HOL/Library/Fraction_Field.thy Fri Oct 12 18:58:20 2012 +0200 @@ -55,7 +55,7 @@ definition "fract = {(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel" -typedef (open) 'a fract = "fract :: ('a * 'a::idom) set set" +typedef 'a fract = "fract :: ('a * 'a::idom) set set" unfolding fract_def proof have "(0::'a, 1::'a) \<in> {x. snd x \<noteq> 0}" by simp