# 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 \ 'a set \ 'a set" ("Idl\ _" [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 \ carrier L & g \ A & (ALL x : A. x \ g)" -text {* Could weaken these to @{term [locale=weak_partial_order] "l \ carrier L \ l - .\ A"} and @{term [locale=weak_partial_order] "g \ carrier L \ g .\ A"}. *} +text (in weak_partial_order) {* Could weaken these to @{term "l \ carrier L \ l + .\ A"} and @{term "g \ carrier L \ g .\ A"}. *} lemma least_closed [intro, simp]: "least L l A ==> l \ carrier L" @@ -306,8 +306,8 @@ "[| x .= x'; x \ carrier L; x' \ 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 \ k \\<^bsub>P\<^esub> monom P \ 1 = monom P \ 1 \\<^bsub>P\<^esub> monom P \ k" unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..