diff -r b716b16ab2ac -r e72e44cee6f2 src/HOL/IMP/Abs_Int_init.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Abs_Int_init.thy	Thu Apr 19 20:19:13 2012 +0200
@@ -0,0 +1,9 @@
+theory Abs_Int_init
+imports "~~/src/HOL/ex/Interpretation_with_Defs"
+        "~~/src/HOL/Library/While_Combinator"
+        Vars Collecting Abs_Int_Tests
+begin
+
+hide_const (open) top bot dom --"to avoid qualified names"
+
+end