src/ZF/UNITY/WFair.thy

--- a/src/ZF/UNITY/WFair.thy	Sun Apr 09 20:17:00 2017 +0200
+++ b/src/ZF/UNITY/WFair.thy	Sun Apr 09 20:44:35 2017 +0200
@@ -6,7 +6,7 @@
 section\<open>Progress under Weak Fairness\<close>
 
 theory WFair
-imports UNITY Main_ZFC
+imports UNITY ZFC
 begin
 
 text\<open>This theory defines the operators transient, ensures and leadsTo,