src/HOL/Algebra/FiniteProduct.thy

 
 subsection \<open>Product Operator for Commutative Monoids\<close>
 
 subsubsection \<open>Inductive Definition of a Relation for Products over Sets\<close>
 
-text \<open>Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
+text \<open>Instantiation of locale \<open>LC\<close> of theory \<open>Finite_Set\<close> is not
   possible, because here we have explicit typing rules like 
-  @{text "x \<in> carrier G"}.  We introduce an explicit argument for the domain
-  @{text D}.\<close>
+  \<open>x \<in> carrier G\<close>.  We introduce an explicit argument for the domain
+  \<open>D\<close>.\<close>
 
 inductive_set
   foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
   for D :: "'a set" and f :: "'b => 'a => 'a" and e :: 'a
   where

   apply (erule foldSetD.cases)
    apply blast
   apply (erule foldSetD.cases)
    apply blast
   apply clarify
-  txt \<open>force simplification of @{text "card A < card (insert ...)"}.\<close>
+  txt \<open>force simplification of \<open>card A < card (insert ...)\<close>.\<close>
   apply (erule rev_mp)
   apply (simp add: less_Suc_eq_le)
   apply (rule impI)
   apply (rename_tac xa Aa ya xb Ab yb, case_tac "xa = xb")
    apply (subgoal_tac "Aa = Ab")

 lemma (in LCD) foldD_nest_Un_disjoint:
   "[| finite A; finite B; A Int B = {}; e \<in> D; A \<subseteq> B; C \<subseteq> B |]
     ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
   by (simp add: foldD_nest_Un_Int)
 
--- \<open>Delete rules to do with @{text foldSetD} relation.\<close>
+\<comment> \<open>Delete rules to do with \<open>foldSetD\<close> relation.\<close>
 
 declare foldSetD_imp_finite [simp del]
   empty_foldSetDE [rule del]
   foldSetD.intros [rule del]
 declare (in LCD)

 
 
 text \<open>Commutative Monoids\<close>
 
 text \<open>
-  We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"}
-  instead of @{text "'b => 'a => 'a"}.
+  We enter a more restrictive context, with \<open>f :: 'a => 'a => 'a\<close>
+  instead of \<open>'b => 'a => 'a\<close>.
 \<close>
 
 locale ACeD =
   fixes D :: "'a set"
     and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)

 syntax
   "_finprod" :: "index => idt => 'a set => 'b => 'b"
       ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
   "\<Otimes>\<^bsub>G\<^esub>i\<in>A. b" \<rightleftharpoons> "CONST finprod G (%i. b) A"
-  -- \<open>Beware of argument permutation!\<close>
+  \<comment> \<open>Beware of argument permutation!\<close>
 
 lemma (in comm_monoid) finprod_empty [simp]: 
   "finprod G f {} = \<one>"
   by (simp add: finprod_def)
 

 
 lemma finprod_Un_Int:
   "[| finite A; finite B; g \<in> A \<rightarrow> carrier G; g \<in> B \<rightarrow> carrier G |] ==>
      finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
      finprod G g A \<otimes> finprod G g B"
--- \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
+\<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
 proof (induct set: finite)
   case empty then show ?case by simp
 next
   case (insert a A)
   then have a: "g a \<in> carrier G" by fast

       !!i. i \<in> B =simp=> f i = g i |] ==> finprod G f A = finprod G g B"
   (* This order of prems is slightly faster (3%) than the last two swapped. *)
   by (rule finprod_cong') (auto simp add: simp_implies_def)
 
 text \<open>Usually, if this rule causes a failed congruence proof error,
-  the reason is that the premise @{text "g \<in> B \<rightarrow> carrier G"} cannot be shown.
+  the reason is that the premise \<open>g \<in> B \<rightarrow> carrier G\<close> cannot be shown.
   Adding @{thm [source] Pi_def} to the simpset is often useful.
   For this reason, @{thm [source] finprod_cong}
   is not added to the simpset by default.
 \<close>