equal
deleted
inserted
replaced
8 |
8 |
9 theory Euclid |
9 theory Euclid |
10 imports |
10 imports |
11 "~~/src/HOL/Number_Theory/UniqueFactorization" |
11 "~~/src/HOL/Number_Theory/UniqueFactorization" |
12 Util |
12 Util |
13 "~~/src/HOL/Library/Efficient_Nat" |
13 "~~/src/HOL/Library/Code_Target_Numeral" |
14 begin |
14 begin |
15 |
15 |
16 text {* |
16 text {* |
17 A constructive version of the proof of Euclid's theorem by |
17 A constructive version of the proof of Euclid's theorem by |
18 Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}. |
18 Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}. |