# HG changeset patch # User wenzelm # Date 1204749239 -3600 # Node ID 51f8a696cd8da298430ef2bee3d5546572003e3a # Parent d3363a8547083075bd7526b240298fd513631435 explicit referencing of background facts; diff -r d3363a854708 -r 51f8a696cd8d src/HOL/Algebra/Ring.thy --- 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 *} diff -r d3363a854708 -r 51f8a696cd8d src/HOL/Algebra/UnivPoly.thy --- 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 \\<^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)