--- a/src/HOL/Algebra/Ideal.thy Sun Mar 08 17:05:43 2009 +0100
+++ b/src/HOL/Algebra/Ideal.thy Sun Mar 08 17:19:15 2009 +0100
@@ -45,7 +45,7 @@
done
qed
-subsubsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
+subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
constdefs (structure R)
genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)
@@ -346,8 +346,7 @@
qed
-subsection {* Ideals generated by a subset of @{term [locale=ring]
- "carrier R"} *}
+subsection (in ring) {* Ideals generated by a subset of @{term "carrier R"} *}
text {* @{term genideal} generates an ideal *}
lemma (in ring) genideal_ideal:
--- a/src/HOL/Algebra/Lattice.thy Sun Mar 08 17:05:43 2009 +0100
+++ b/src/HOL/Algebra/Lattice.thy Sun Mar 08 17:19:15 2009 +0100
@@ -282,8 +282,8 @@
greatest :: "[_, 'a, 'a set] => bool"
"greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
-text {* Could weaken these to @{term [locale=weak_partial_order] "l \<in> carrier L \<and> l
- .\<in> A"} and @{term [locale=weak_partial_order] "g \<in> carrier L \<and> g .\<in> A"}. *}
+text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
+ .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
lemma least_closed [intro, simp]:
"least L l A ==> l \<in> carrier L"
@@ -306,8 +306,8 @@
"[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
by (unfold least_def) (auto dest: sym)
-text {* @{const least} is not congruent in the second parameter for
- @{term [locale=weak_partial_order] "A {.=} A'"} *}
+text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for
+ @{term "A {.=} A'"} *}
lemma (in weak_partial_order) least_Upper_cong_l:
assumes "x .= x'"
@@ -363,8 +363,8 @@
greatest L x A = greatest L x' A"
by (unfold greatest_def) (auto dest: sym)
-text {* @{const greatest} is not congruent in the second parameter for
- @{term [locale=weak_partial_order] "A {.=} A'"} *}
+text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for
+ @{term "A {.=} A'"} *}
lemma (in weak_partial_order) greatest_Lower_cong_l:
assumes "x .= x'"
--- a/src/HOL/Algebra/UnivPoly.thy Sun Mar 08 17:05:43 2009 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Sun Mar 08 17:19:15 2009 +0100
@@ -190,7 +190,7 @@
context UP
begin
-text {*Temporarily declare @{thm [locale=UP] P_def} as simp rule.*}
+text {*Temporarily declare @{thm P_def} as simp rule.*}
declare P_def [simp]
@@ -638,8 +638,8 @@
}
qed
-text{*The following corollary follows from lemmas @{thm [locale=UP_ring] "monom_one_Suc"}
- and @{thm [locale=UP_ring] "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
+text{*The following corollary follows from lemmas @{thm "monom_one_Suc"}
+ and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..