src/HOL/IMP/Abs_Int_init.thy
changeset 51389 8a9f0503b1c0
parent 47613 e72e44cee6f2
child 51390 1dff81cf425b
--- a/src/HOL/IMP/Abs_Int_init.thy	Sun Mar 10 14:36:18 2013 +0100
+++ b/src/HOL/IMP/Abs_Int_init.thy	Sun Mar 10 18:29:10 2013 +0100
@@ -1,6 +1,5 @@
 theory Abs_Int_init
-imports "~~/src/HOL/ex/Interpretation_with_Defs"
-        "~~/src/HOL/Library/While_Combinator"
+imports "~~/src/HOL/Library/While_Combinator"
         Vars Collecting Abs_Int_Tests
 begin