changeset 65417 | fc41a5650fb1 |
parent 63830 | 2ea3725a34bd |
child 66258 | 2b83dd24b301 |
65416:f707dbcf11e3 | 65417:fc41a5650fb1 |
---|---|
6 |
6 |
7 section \<open>Euclid's theorem\<close> |
7 section \<open>Euclid's theorem\<close> |
8 |
8 |
9 theory Euclid |
9 theory Euclid |
10 imports |
10 imports |
11 "~~/src/HOL/Number_Theory/Primes" |
11 "~~/src/HOL/Computational_Algebra/Primes" |
12 Util |
12 Util |
13 "~~/src/HOL/Library/Code_Target_Numeral" |
13 "~~/src/HOL/Library/Code_Target_Numeral" |
14 begin |
14 begin |
15 |
15 |
16 text \<open> |
16 text \<open> |