src/HOL/Old_Number_Theory/Factorization.thy
changeset 61382 efac889fccbc
parent 58889 5b7a9633cfa8
child 62481 b5d8e57826df
     1.1 --- a/src/HOL/Old_Number_Theory/Factorization.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Factorization.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -3,14 +3,14 @@
     1.4      Copyright   2000  University of Cambridge
     1.5  *)
     1.6  
     1.7 -section {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
     1.8 +section \<open>Fundamental Theorem of Arithmetic (unique factorization into primes)\<close>
     1.9  
    1.10  theory Factorization
    1.11  imports Primes "~~/src/HOL/Library/Permutation"
    1.12  begin
    1.13  
    1.14  
    1.15 -subsection {* Definitions *}
    1.16 +subsection \<open>Definitions\<close>
    1.17  
    1.18  definition primel :: "nat list => bool"
    1.19    where "primel xs = (\<forall>p \<in> set xs. prime p)"
    1.20 @@ -36,7 +36,7 @@
    1.21  | "sort (x # xs) = oinsert x (sort xs)"
    1.22  
    1.23  
    1.24 -subsection {* Arithmetic *}
    1.25 +subsection \<open>Arithmetic\<close>
    1.26  
    1.27  lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> Suc 0 ==> Suc 0 < m"
    1.28    apply (cases m)
    1.29 @@ -64,7 +64,7 @@
    1.30    done
    1.31  
    1.32  
    1.33 -subsection {* Prime list and product *}
    1.34 +subsection \<open>Prime list and product\<close>
    1.35  
    1.36  lemma prod_append: "prod (xs @ ys) = prod xs * prod ys"
    1.37    apply (induct xs)
    1.38 @@ -137,7 +137,7 @@
    1.39    done
    1.40  
    1.41  
    1.42 -subsection {* Sorting *}
    1.43 +subsection \<open>Sorting\<close>
    1.44  
    1.45  lemma nondec_oinsert: "nondec xs \<Longrightarrow> nondec (oinsert x xs)"
    1.46    apply (induct xs)
    1.47 @@ -174,7 +174,7 @@
    1.48    done
    1.49  
    1.50  
    1.51 -subsection {* Permutation *}
    1.52 +subsection \<open>Permutation\<close>
    1.53  
    1.54  lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys"
    1.55    apply (unfold primel_def)
    1.56 @@ -212,7 +212,7 @@
    1.57    done
    1.58  
    1.59  
    1.60 -subsection {* Existence *}
    1.61 +subsection \<open>Existence\<close>
    1.62  
    1.63  lemma ex_nondec_lemma:
    1.64      "primel xs ==> \<exists>ys. primel ys \<and> nondec ys \<and> prod ys = prod xs"
    1.65 @@ -250,7 +250,7 @@
    1.66    done
    1.67  
    1.68  
    1.69 -subsection {* Uniqueness *}
    1.70 +subsection \<open>Uniqueness\<close>
    1.71  
    1.72  lemma prime_dvd_mult_list [rule_format]:
    1.73      "prime p ==> p dvd (prod xs) --> (\<exists>m. m:set xs \<and> p dvd m)"