src/ZF/Constructible/Wellorderings.thy
changeset 16417 9bc16273c2d4
parent 13780 af7b79271364
child 21233 5a5c8ea5f66a
--- a/src/ZF/Constructible/Wellorderings.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
 
 header {*Relativized Wellorderings*}
 
-theory Wellorderings = Relative:
+theory Wellorderings imports Relative begin
 
 text{*We define functions analogous to @{term ordermap} @{term ordertype} 
       but without using recursion.  Instead, there is a direct appeal