proper local context for text with antiquotations;
authorwenzelm
Sun Mar 08 17:19:15 2009 +0100 (2009-03-08)
changeset 303639b8d9b6ef803
parent 30362 4ec39edb88b1
child 30364 577edc39b501
proper local context for text with antiquotations;
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/UnivPoly.thy
     1.1 --- a/src/HOL/Algebra/Ideal.thy	Sun Mar 08 17:05:43 2009 +0100
     1.2 +++ b/src/HOL/Algebra/Ideal.thy	Sun Mar 08 17:19:15 2009 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4    done
     1.5  qed
     1.6  
     1.7 -subsubsection {* Ideals Generated by a Subset of @{term [locale=ring] "carrier R"} *}
     1.8 +subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
     1.9  
    1.10  constdefs (structure R)
    1.11    genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
    1.12 @@ -346,8 +346,7 @@
    1.13  qed
    1.14  
    1.15  
    1.16 -subsection {* Ideals generated by a subset of @{term [locale=ring]
    1.17 -  "carrier R"} *}
    1.18 +subsection (in ring) {* Ideals generated by a subset of @{term "carrier R"} *}
    1.19  
    1.20  text {* @{term genideal} generates an ideal *}
    1.21  lemma (in ring) genideal_ideal:
     2.1 --- a/src/HOL/Algebra/Lattice.thy	Sun Mar 08 17:05:43 2009 +0100
     2.2 +++ b/src/HOL/Algebra/Lattice.thy	Sun Mar 08 17:19:15 2009 +0100
     2.3 @@ -282,8 +282,8 @@
     2.4    greatest :: "[_, 'a, 'a set] => bool"
     2.5    "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
     2.6  
     2.7 -text {* Could weaken these to @{term [locale=weak_partial_order] "l \<in> carrier L \<and> l
     2.8 -  .\<in> A"} and @{term [locale=weak_partial_order] "g \<in> carrier L \<and> g .\<in> A"}. *}
     2.9 +text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
    2.10 +  .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
    2.11  
    2.12  lemma least_closed [intro, simp]:
    2.13    "least L l A ==> l \<in> carrier L"
    2.14 @@ -306,8 +306,8 @@
    2.15    "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
    2.16    by (unfold least_def) (auto dest: sym)
    2.17  
    2.18 -text {* @{const least} is not congruent in the second parameter for 
    2.19 -  @{term [locale=weak_partial_order] "A {.=} A'"} *}
    2.20 +text (in weak_partial_order) {* @{const least} is not congruent in the second parameter for 
    2.21 +  @{term "A {.=} A'"} *}
    2.22  
    2.23  lemma (in weak_partial_order) least_Upper_cong_l:
    2.24    assumes "x .= x'"
    2.25 @@ -363,8 +363,8 @@
    2.26    greatest L x A = greatest L x' A"
    2.27    by (unfold greatest_def) (auto dest: sym)
    2.28  
    2.29 -text {* @{const greatest} is not congruent in the second parameter for 
    2.30 -  @{term [locale=weak_partial_order] "A {.=} A'"} *}
    2.31 +text (in weak_partial_order) {* @{const greatest} is not congruent in the second parameter for 
    2.32 +  @{term "A {.=} A'"} *}
    2.33  
    2.34  lemma (in weak_partial_order) greatest_Lower_cong_l:
    2.35    assumes "x .= x'"
     3.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Mar 08 17:05:43 2009 +0100
     3.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sun Mar 08 17:19:15 2009 +0100
     3.3 @@ -190,7 +190,7 @@
     3.4  context UP
     3.5  begin
     3.6  
     3.7 -text {*Temporarily declare @{thm [locale=UP] P_def} as simp rule.*}
     3.8 +text {*Temporarily declare @{thm P_def} as simp rule.*}
     3.9  
    3.10  declare P_def [simp]
    3.11  
    3.12 @@ -638,8 +638,8 @@
    3.13    }
    3.14  qed
    3.15  
    3.16 -text{*The following corollary follows from lemmas @{thm [locale=UP_ring] "monom_one_Suc"} 
    3.17 -  and @{thm [locale=UP_ring] "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
    3.18 +text{*The following corollary follows from lemmas @{thm "monom_one_Suc"} 
    3.19 +  and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
    3.20  
    3.21  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"
    3.22    unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..