src/ZF/IMP/Com.thy

--- a/src/ZF/IMP/Com.thy	Sun Apr 09 20:17:00 2017 +0200
+++ b/src/ZF/IMP/Com.thy	Sun Apr 09 20:44:35 2017 +0200
@@ -4,7 +4,7 @@
 
 section \<open>Arithmetic expressions, boolean expressions, commands\<close>
 
-theory Com imports Main begin
+theory Com imports ZF begin
 
 
 subsection \<open>Arithmetic expressions\<close>