# HG changeset patch
# User wenzelm
# Date 1236529155 -3600
# Node ID 9b8d9b6ef80378d0bb6e3012c41312768aa222a6
# Parent  4ec39edb88b131a26cd66b812d8ff0ecaf560a11
proper local context for text with antiquotations;

diff -r 4ec39edb88b1 -r 9b8d9b6ef803 src/HOL/Algebra/Ideal.thy
--- 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:
diff -r 4ec39edb88b1 -r 9b8d9b6ef803 src/HOL/Algebra/Lattice.thy
--- 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'"
diff -r 4ec39edb88b1 -r 9b8d9b6ef803 src/HOL/Algebra/UnivPoly.thy
--- 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] ..