src/ZF/UNITY/Guar.thy
changeset 16417 9bc16273c2d4
parent 14093 24382760fd89
child 24893 b8ef7afe3a6b
--- a/src/ZF/UNITY/Guar.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/Guar.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -22,7 +22,7 @@
 
 header{*The Chandy-Sanders Guarantees Operator*}
 
-theory Guar = Comp: 
+theory Guar imports Comp begin 
 
 
 (* To be moved to theory WFair???? *)