# HG changeset patch
# User lcp
# Date 794578898 -3600
# Node ID 63f02d32509e21d7dcf260db570d99d08a811773
# Parent  137035296ad635e5f72007e682f8662d0a1f5fa5
Replaced rules by defs

diff -r 137035296ad6 -r 63f02d32509e src/ZF/Coind/ECR.thy
--- a/src/ZF/Coind/ECR.thy	Tue Mar 07 13:18:48 1995 +0100
+++ b/src/ZF/Coind/ECR.thy	Tue Mar 07 13:21:38 1995 +0100
@@ -29,10 +29,10 @@
  
 consts
   hastyenv :: "[i,i] => o"
-rules
+defs
   hastyenv_def 
-    " hastyenv(ve,te) == \
-\     ve_dom(ve) = te_dom(te) & \
+    " hastyenv(ve,te) == 			\
+\     ve_dom(ve) = te_dom(te) & 		\
 \     (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
 
 end
diff -r 137035296ad6 -r 63f02d32509e src/ZF/WF.thy
--- a/src/ZF/WF.thy	Tue Mar 07 13:18:48 1995 +0100
+++ b/src/ZF/WF.thy	Tue Mar 07 13:21:38 1995 +0100
@@ -16,7 +16,7 @@
   is_recfun    :: "[i, i, [i,i]=>i, i] =>o"
   the_recfun   :: "[i, i, [i,i]=>i] =>i"
 
-rules
+defs
   (*r is a well-founded relation*)
   wf_def	 "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"