src/HOL/Number_Theory/UniqueFactorization.thy

 Note: there were previous Isabelle formalizations of unique
 factorization due to Thomas Marthedal Rasmussen, and, building on
 that, by Jeremy Avigad and David Gray.  
 *)
 
-section {* UniqueFactorization *}
+section \<open>UniqueFactorization\<close>
 
 theory UniqueFactorization
 imports Cong "~~/src/HOL/Library/Multiset"
 begin
 

    semirings, using of_nat. Also, is it worth developing bounded quantifiers 
    "ALL i :# M. P i"? 
 *)
 
 
-subsection {* unique factorization: multiset version *}
+subsection \<open>unique factorization: multiset version\<close>
 
 lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> 
     (EX M. (ALL (p::nat) : set_mset M. prime p) & n = (PROD i :# M. i))"
 proof (rule nat_less_induct, clarify)
   fix n :: nat

   apply (insert multiset_prime_factorization_unique)
   apply auto
 done
 
 
-subsection {* Prime factors and multiplicity for nats and ints *}
+subsection \<open>Prime factors and multiplicity for nats and ints\<close>
 
 class unique_factorization =
   fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
     and prime_factors :: "'a \<Rightarrow> 'a set"
 

 instance ..
 
 end
 
 
-subsection {* Set up transfer *}
+subsection \<open>Set up transfer\<close>
 
 lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
   unfolding prime_factors_int_def
   apply auto
   apply (subst transfer_int_nat_set_return_embed)

 declare transfer_morphism_int_nat[transfer add return: 
   transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
   transfer_int_nat_multiplicity]
 
 
-subsection {* Properties of prime factors and multiplicity for nats and ints *}
+subsection \<open>Properties of prime factors and multiplicity for nats and ints\<close>
 
 lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
   unfolding prime_factors_int_def by auto
 
 lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"

     apply force
     apply force
     using assms
     apply (simp add: set_mset_def msetprod_multiplicity)
     done
-  with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
+  with \<open>f \<in> multiset\<close> have "count (multiset_prime_factorization n) = f"
     by simp
   with S_eq show ?thesis
     by (simp add: set_mset_def multiset_def prime_factors_nat_def multiplicity_nat_def)
 qed
 

   apply (rule dvd_antisym [transferred])
   apply (auto intro: multiplicity_dvd'_int) 
   done
 
 
-subsection {* An application *}
+subsection \<open>An application\<close>
 
 lemma gcd_eq_nat: 
   assumes pos [arith]: "x > 0" "y > 0"
   shows "gcd (x::nat) y = 
     (PROD p: prime_factors x Un prime_factors y.