# HG changeset patch
# User wenzelm
# Date 1082116363 -7200
# Node ID 276ef51cedbf76104a758f7758f7f9ec0814b573
# Parent  feae7b5fd4257ccddbc59515104c4ee98c3ae3c7
simplified ML code for setsubgoaler;

diff -r feae7b5fd425 -r 276ef51cedbf src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Fri Apr 16 13:51:04 2004 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Apr 16 13:52:43 2004 +0200
@@ -291,8 +291,7 @@
    like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
 
 ML_setup {* 
-  Context.>> (fn thy => (simpset_ref_of thy :=
-    simpset_of thy setsubgoaler asm_full_simp_tac; thy))
+  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
 *}
 
 lemma (in comm_monoid) finprod_empty [simp]: 
@@ -300,8 +299,7 @@
   by (simp add: finprod_def)
 
 ML_setup {* 
-  Context.>> (fn thy => (simpset_ref_of thy :=
-    simpset_of thy setsubgoaler asm_simp_tac; thy))
+  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
 *}
 
 declare funcsetI [intro]
diff -r feae7b5fd425 -r 276ef51cedbf src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 13:51:04 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 13:52:43 2004 +0200
@@ -295,8 +295,8 @@
   by (rule up_eqI, simp add: a_comm R, simp_all add: R)
 
 ML_setup {*
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+  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"
@@ -328,8 +328,8 @@
 qed (simp_all add: R)
 
 ML_setup {*
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
+  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
+*}
 
 lemma (in UP_cring) UP_l_one [simp]:
   assumes R: "p \<in> carrier P"
@@ -618,8 +618,8 @@
   by (simp add: UP_def P_def)
 
 ML_setup {*
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+  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"
@@ -639,8 +639,8 @@
 qed (simp_all add: R)
 
 ML_setup {*
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
+  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
+*}
 
 lemma (in UP_cring) monom_add [simp]:
   "[| a \<in> carrier R; b \<in> carrier R |] ==>
@@ -648,8 +648,8 @@
   by (rule up_eqI) simp_all
 
 ML_setup {*
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+  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>\<^sub>2 monom P \<one> 1"
@@ -725,8 +725,8 @@
 qed (simp_all)
 
 ML_setup {*
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
+  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>\<^sub>2 monom P b n"
@@ -977,8 +977,8 @@
 qed (simp add: R)
 
 ML_setup {*
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
+*}
 
 lemma (in UP_domain) deg_mult [simp]:
   "[| p ~= \<zero>\<^sub>2; q ~= \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P |] ==>
@@ -1017,8 +1017,8 @@
   using fin by induct (auto simp: Pi_def)
 
 ML_setup {*
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
+*}
 
 lemma (in UP_cring) up_repr:
   assumes R: "p \<in> carrier P"
@@ -1073,8 +1073,8 @@
 qed
 
 ML_setup {*
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
+  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
+*}
 
 subsection {* Polynomials over an integral domain form an integral domain *}
 
@@ -1153,8 +1153,8 @@
 subsection {* Evaluation Homomorphism and Universal Property*}
 
 ML_setup {*
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
+*}
 
 (* alternative congruence rule (possibly more efficient)
 lemma (in abelian_monoid) finsum_cong2:
@@ -1493,7 +1493,6 @@
     by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
   have Psi_hom: "ring_hom_cring P S Psi"
     by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
-thm monom_mult
   have "Phi p = Phi (finsum P
     (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
     by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
@@ -1568,4 +1567,4 @@
 -- {* Calculates @{term "x = 500"} *}
 
 
-end
\ No newline at end of file
+end
diff -r feae7b5fd425 -r 276ef51cedbf src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Apr 16 13:51:04 2004 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Apr 16 13:52:43 2004 +0200
@@ -36,11 +36,11 @@
    This makes setsum_cong more convenient to use, because assumptions
    like i:{m..n} get simplified (to m <= i & i <= n). *)
 
-ML_setup {* 
+declare setsum_cong [cong]
 
-Addcongs [thm "setsum_cong"];
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
+ML_setup {* 
+  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
+*}
 
 section {* Definition of type up *}
 
@@ -776,4 +776,4 @@
   "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
 by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
 
-end
\ No newline at end of file
+end
diff -r feae7b5fd425 -r 276ef51cedbf src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Apr 16 13:51:04 2004 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 16 13:52:43 2004 +0200
@@ -1022,15 +1022,13 @@
 
   end);  (* struct *)
 
-Context.>> (fn thy => (simpset_ref_of thy :=
-  simpset_of thy
+simpset_ref() := simpset ()
     addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac))
     addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac));
   (* Adding the transitivity reasoners also as safe solvers showed a slight
      speed up, but the reasoning strength appears to be not higher (at least
      no breaking of additional proofs in the entire HOL distribution, as
      of 5 March 2004, was observed). *)
-  thy))
 *}
 
 (* Optional methods