src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy
changeset 48480 cb03acfae211
parent 47818 151d137f1095
child 51698 c0af8bbc5825
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Tue Jul 24 17:33:19 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy	Tue Jul 24 17:34:46 2012 +0200
@@ -1,7 +1,7 @@
 (* Author: Tobias Nipkow *)
 
 theory Abs_Int2_ITP
-imports Abs_Int1_ITP Vars
+imports Abs_Int1_ITP "../Vars"
 begin
 
 instantiation prod :: (preord,preord) preord