src/HOL/Algebra/Sym_Groups.thy

 qed
 
 
 subsection \<open>Unsolvability of Symmetric Groups\<close>
 
-text \<open>We show that symmetric groups (@{term\<open>sym_group n\<close>}) are unsolvable for @{term\<open>n \<ge> 5\<close>}.\<close>
+text \<open>We show that symmetric groups (\<^term>\<open>sym_group n\<close>) are unsolvable for \<^term>\<open>n \<ge> 5\<close>.\<close>
 
 abbreviation three_cycles :: "nat \<Rightarrow> (nat \<Rightarrow> nat) set"
   where "three_cycles n \<equiv>
            { cycle_of_list cs | cs. cycle cs \<and> length cs = 3 \<and> set cs \<subseteq> {1..n} }"