--- 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]
--- 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
--- 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
--- 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