# HG changeset patch
# User wenzelm
# Date 1331994788 -3600
# Node ID 196f2d9406c4d0d3782640cb2b79258c0c1766f1
# Parent  63fae4a2cc65e33c9cfaba18015c4804f6ca80ed
tuned proofs;

diff -r 63fae4a2cc65 -r 196f2d9406c4 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Mar 17 14:01:09 2012 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Mar 17 15:33:08 2012 +0100
@@ -1130,10 +1130,10 @@
 lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
   by (simp add: shift1_def)
 lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p "
-  by (induct k arbitrary: p, auto simp add: shift1_degree)
+  by (induct k arbitrary: p) (auto simp add: shift1_degree)
 
 lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p"
-  by (induct n arbitrary: p, simp_all add: funpow_def)
+  by (induct n arbitrary: p) (simp_all add: funpow.simps)
 
 lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p"
   by (induct p arbitrary: n rule: degree.induct, auto)