equal
deleted
inserted
replaced
8 |
8 |
9 theory Euclid |
9 theory Euclid |
10 imports |
10 imports |
11 "HOL-Computational_Algebra.Primes" |
11 "HOL-Computational_Algebra.Primes" |
12 Util |
12 Util |
13 "HOL-Library.Old_Datatype" |
|
14 "HOL-Library.Code_Target_Numeral" |
13 "HOL-Library.Code_Target_Numeral" |
|
14 "HOL-Library.Realizers" |
15 begin |
15 begin |
16 |
16 |
17 text \<open> |
17 text \<open> |
18 A constructive version of the proof of Euclid's theorem by |
18 A constructive version of the proof of Euclid's theorem by |
19 Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}. |
19 Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}. |