src/HOL/Algebra/poly/UnivPoly2.thy
changeset 31001 7e6ffd8f51a9
parent 30968 10fef94f40fc
child 31021 53642251a04f
     1.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Apr 27 08:22:37 2009 +0200
     1.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Apr 27 10:11:44 2009 +0200
     1.3 @@ -345,11 +345,10 @@
     1.4      by (simp add: up_inverse_def)
     1.5    show "p / q = p * inverse q"
     1.6      by (simp add: up_divide_def)
     1.7 -  show "p * 1 = p"
     1.8 -    unfolding `p * 1 = 1 * p` by (fact `1 * p = p`)
     1.9  qed
    1.10  
    1.11 -instance up :: (ring) recpower ..
    1.12 +instance up :: (ring) recpower proof
    1.13 +qed simp_all
    1.14  
    1.15  (* Further properties of monom *)
    1.16