changeset 64785 | ae0bbc8e45ad |
parent 64784 | 5cb5e7ecb284 |
child 64786 | 340db65fd2c1 |
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jan 04 21:28:28 2017 +0100 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jan 04 21:28:29 2017 +0100 @@ -7,7 +7,6 @@ theory Euclidean_Algorithm imports "~~/src/HOL/GCD" "~~/src/HOL/Number_Theory/Factorial_Ring" - "~~/src/HOL/Number_Theory/Euclidean_Division" begin context euclidean_semiring