src/HOL/IMP/Abs_Int_init.thy
changeset 51390 1dff81cf425b
parent 51389 8a9f0503b1c0
child 53013 3fbcfa911863
--- a/src/HOL/IMP/Abs_Int_init.thy	Sun Mar 10 18:29:10 2013 +0100
+++ b/src/HOL/IMP/Abs_Int_init.thy	Mon Mar 11 12:27:31 2013 +0100
@@ -1,8 +1,10 @@
 theory Abs_Int_init
 imports "~~/src/HOL/Library/While_Combinator"
+        "~~/src/HOL/Library/Quotient_List"
+        "~~/src/HOL/Library/Extended"
         Vars Collecting Abs_Int_Tests
 begin
 
-hide_const (open) top bot dom --"to avoid qualified names"
+hide_const (open) top bot dom  --"to avoid qualified names"
 
 end