src/HOL/Library/Univ_Poly.thy
changeset 46730 e3b99d0231bc
parent 45129 1fce03e3e8ad
child 49751 5248806bc7ab
     1.1 --- a/src/HOL/Library/Univ_Poly.thy	Tue Feb 28 17:11:18 2012 +0100
     1.2 +++ b/src/HOL/Library/Univ_Poly.thy	Tue Feb 28 20:20:09 2012 +0100
     1.3 @@ -103,7 +103,7 @@
     1.4  lemma pmult_singleton: "[h1] *** p1 = h1 %* p1" by simp
     1.5  end
     1.6  
     1.7 -lemma (in semiring_1) poly_ident_mult[simp]: "1 %* t = t" by (induct "t", auto)
     1.8 +lemma (in semiring_1) poly_ident_mult[simp]: "1 %* t = t" by (induct t) auto
     1.9  
    1.10  lemma (in semiring_0) poly_simple_add_Cons[simp]: "[a] +++ ((0)#t) = (a#t)"
    1.11  by simp