src/ZF/Coind/Static.thy

--- a/src/ZF/Coind/Static.thy	Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/Coind/Static.thy	Sun Oct 07 21:19:31 2007 +0200
@@ -18,8 +18,8 @@
 
 (*Its extension to environments*)
 
-constdefs
-  isofenv :: "[i,i] => o"
+definition
+  isofenv :: "[i,i] => o"  where
    "isofenv(ve,te) ==                
       ve_dom(ve) = te_dom(te) &            
       (\<forall>x \<in> ve_dom(ve).                          
@@ -64,10 +64,6 @@
 declare ElabRel.dom_subset [THEN subsetD, dest]
 
 end
-  
-
-
-
 
 
 
@@ -75,14 +71,3 @@
 
 
 
-
-
-
-
-
-
-
-
-
-
-