diff -r 6061ae1f90f2 -r 9bc16273c2d4 src/HOL/ex/PresburgerEx.thy
--- a/src/HOL/ex/PresburgerEx.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/ex/PresburgerEx.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
 Some examples for Presburger Arithmetic
 *)
 
-theory PresburgerEx = Main:
+theory PresburgerEx imports Main begin
 
 theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
   by presburger