1.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Wed Nov 08 22:24:54 2006 +0100
     1.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Nov 08 23:11:13 2006 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  header {* Quantifier elimination for Presburger arithmetic *}
     1.5  
     1.6  theory Reflected_Presburger
     1.7 -imports Main
     1.8 +imports Main GCD
     1.9  begin
    1.10  
    1.11  (* Shadow syntax for integer terms *)