src/HOL/Algebra/UnivPoly.thy
changeset 14590 276ef51cedbf
parent 14577 dbb95b825244
child 14651 02b8f3bcf7fe
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 13:51:04 2004 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 13:52:43 2004 +0200
     1.3 @@ -295,8 +295,8 @@
     1.4    by (rule up_eqI, simp add: a_comm R, simp_all add: R)
     1.5  
     1.6  ML_setup {*
     1.7 -Context.>> (fn thy => (simpset_ref_of thy :=
     1.8 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
     1.9 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.10 +*}
    1.11  
    1.12  lemma (in UP_cring) UP_m_assoc:
    1.13    assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
    1.14 @@ -328,8 +328,8 @@
    1.15  qed (simp_all add: R)
    1.16  
    1.17  ML_setup {*
    1.18 -Context.>> (fn thy => (simpset_ref_of thy :=
    1.19 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    1.20 +  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    1.21 +*}
    1.22  
    1.23  lemma (in UP_cring) UP_l_one [simp]:
    1.24    assumes R: "p \<in> carrier P"
    1.25 @@ -618,8 +618,8 @@
    1.26    by (simp add: UP_def P_def)
    1.27  
    1.28  ML_setup {*
    1.29 -Context.>> (fn thy => (simpset_ref_of thy :=
    1.30 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    1.31 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.32 +*}
    1.33  
    1.34  lemma (in UP_cring) monom_mult_is_smult:
    1.35    assumes R: "a \<in> carrier R" "p \<in> carrier P"
    1.36 @@ -639,8 +639,8 @@
    1.37  qed (simp_all add: R)
    1.38  
    1.39  ML_setup {*
    1.40 -Context.>> (fn thy => (simpset_ref_of thy :=
    1.41 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    1.42 +  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    1.43 +*}
    1.44  
    1.45  lemma (in UP_cring) monom_add [simp]:
    1.46    "[| a \<in> carrier R; b \<in> carrier R |] ==>
    1.47 @@ -648,8 +648,8 @@
    1.48    by (rule up_eqI) simp_all
    1.49  
    1.50  ML_setup {*
    1.51 -Context.>> (fn thy => (simpset_ref_of thy :=
    1.52 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    1.53 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.54 +*}
    1.55  
    1.56  lemma (in UP_cring) monom_one_Suc:
    1.57    "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1"
    1.58 @@ -725,8 +725,8 @@
    1.59  qed (simp_all)
    1.60  
    1.61  ML_setup {*
    1.62 -Context.>> (fn thy => (simpset_ref_of thy :=
    1.63 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    1.64 +  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    1.65 +*}
    1.66  
    1.67  lemma (in UP_cring) monom_mult_smult:
    1.68    "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^sub>2 monom P b n"
    1.69 @@ -977,8 +977,8 @@
    1.70  qed (simp add: R)
    1.71  
    1.72  ML_setup {*
    1.73 -Context.>> (fn thy => (simpset_ref_of thy :=
    1.74 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    1.75 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.76 +*}
    1.77  
    1.78  lemma (in UP_domain) deg_mult [simp]:
    1.79    "[| p ~= \<zero>\<^sub>2; q ~= \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P |] ==>
    1.80 @@ -1017,8 +1017,8 @@
    1.81    using fin by induct (auto simp: Pi_def)
    1.82  
    1.83  ML_setup {*
    1.84 -Context.>> (fn thy => (simpset_ref_of thy :=
    1.85 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    1.86 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.87 +*}
    1.88  
    1.89  lemma (in UP_cring) up_repr:
    1.90    assumes R: "p \<in> carrier P"
    1.91 @@ -1073,8 +1073,8 @@
    1.92  qed
    1.93  
    1.94  ML_setup {*
    1.95 -Context.>> (fn thy => (simpset_ref_of thy :=
    1.96 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    1.97 +  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    1.98 +*}
    1.99  
   1.100  subsection {* Polynomials over an integral domain form an integral domain *}
   1.101  
   1.102 @@ -1153,8 +1153,8 @@
   1.103  subsection {* Evaluation Homomorphism and Universal Property*}
   1.104  
   1.105  ML_setup {*
   1.106 -Context.>> (fn thy => (simpset_ref_of thy :=
   1.107 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   1.108 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
   1.109 +*}
   1.110  
   1.111  (* alternative congruence rule (possibly more efficient)
   1.112  lemma (in abelian_monoid) finsum_cong2:
   1.113 @@ -1493,7 +1493,6 @@
   1.114      by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
   1.115    have Psi_hom: "ring_hom_cring P S Psi"
   1.116      by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
   1.117 -thm monom_mult
   1.118    have "Phi p = Phi (finsum P
   1.119      (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
   1.120      by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
   1.121 @@ -1568,4 +1567,4 @@
   1.122  -- {* Calculates @{term "x = 500"} *}
   1.123  
   1.124  
   1.125 -end
   1.126 \ No newline at end of file
   1.127 +end