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)"
```