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