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