src/ZF/Coind/Static.thy

--- a/src/ZF/Coind/Static.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Coind/Static.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -4,7 +4,7 @@
     Copyright   1995  University of Cambridge
 *)
 
-theory Static = Values + Types:
+theory Static imports Values Types begin
 
 (*** Basic correspondence relation -- not completely specified, as it is a
      parameter of the proof.  A concrete version could be defined inductively.