--- a/src/HOL/Algebra/Ring.thy Wed Mar 05 21:24:07 2008 +0100
+++ b/src/HOL/Algebra/Ring.thy Wed Mar 05 21:33:59 2008 +0100
@@ -362,7 +362,7 @@
lemma (in ring) is_ring:
"ring R"
- by fact
+ by (rule ring_axioms)
lemmas ring_record_simps = monoid_record_simps ring.simps
@@ -399,7 +399,7 @@
by (auto intro!: comm_monoidI m_assoc m_comm)
lemma (in cring) is_cring:
- "cring R" by fact
+ "cring R" by (rule cring_axioms)
subsubsection {* Normaliser for Rings *}
--- a/src/HOL/Algebra/UnivPoly.thy Wed Mar 05 21:24:07 2008 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Mar 05 21:33:59 2008 +0100
@@ -1229,7 +1229,7 @@
shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
proof -
interpret UP_univ_prop [R S h P s _]
- using `UP_pre_univ_prop R S h` P_def R S
+ using UP_pre_univ_prop_axioms P_def R S
by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
from R
show ?thesis by (rule Eval_monom)