# HG changeset patch
# User berghofe
# Date 1120219430 -7200
# Node ID 5a89d3622ac01c41e52273f9f143a6acc5a5c897
# Parent  3dc904d93767fa1a8783df2eeb1f7eb0e81738cc
Removed setsubgoaler hack (thanks to strengthened finsum_cong).

diff -r 3dc904d93767 -r 5a89d3622ac0 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Jul 01 14:02:58 2005 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Jul 01 14:03:50 2005 +0200
@@ -285,10 +285,6 @@
   shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p"
   by (rule up_eqI, simp add: a_comm R, simp_all add: R)
 
-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
 lemma (in UP_cring) UP_m_assoc:
   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
@@ -318,10 +314,6 @@
     by (simp add: Pi_def)
 qed (simp_all add: R)
 
-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
-*}
-
 lemma (in UP_cring) UP_l_one [simp]:
   assumes R: "p \<in> carrier P"
   shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p"
@@ -630,10 +622,6 @@
   "monom P \<zero> n = \<zero>\<^bsub>P\<^esub>"
   by (simp add: UP_def P_def)
 
-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
 lemma (in UP_cring) monom_mult_is_smult:
   assumes R: "a \<in> carrier R" "p \<in> carrier P"
   shows "monom P a 0 \<otimes>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p"
@@ -651,19 +639,11 @@
     by (simp add: UP_m_comm)
 qed (simp_all add: R)
 
-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
-*}
-
 lemma (in UP_cring) monom_add [simp]:
   "[| a \<in> carrier R; b \<in> carrier R |] ==>
   monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n"
   by (rule up_eqI) simp_all
 
-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
 lemma (in UP_cring) monom_one_Suc:
   "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
 proof (rule up_eqI)
@@ -739,10 +719,6 @@
   qed
 qed (simp_all)
 
-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
-*}
-
 lemma (in UP_cring) monom_mult_smult:
   "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^bsub>P\<^esub> monom P b n"
   by (rule up_eqI) simp_all
@@ -993,10 +969,6 @@
   with boundm R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) m = \<zero>" by simp
 qed (simp add: R)
 
-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
 lemma (in UP_domain) deg_mult [simp]:
   "[| p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
   deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
@@ -1033,10 +1005,6 @@
     coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
   using fin by induct (auto simp: Pi_def)
 
-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
 lemma (in UP_cring) up_repr:
   assumes R: "p \<in> carrier P"
   shows "(\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
@@ -1089,10 +1057,6 @@
   finally show ?thesis .
 qed
 
-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
-*}
-
 subsection {* Polynomials over an integral domain form an integral domain *}
 
 lemma domainI:
@@ -1178,10 +1142,6 @@
   !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
   sorry*)
 
-ML_setup {*
-  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
-*}
-
 theorem (in cring) diagonal_sum:
   "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
   (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =