# HG changeset patch
# User lcp
# Date 794741910 -3600
# Node ID 23df3da5ffb53ac0027bfb6f47e4ff1253f9b4ae
# Parent  01d6571fa10643b176eb0fc9e8a501ad1a45f940
Commented isof(c,t)

diff -r 01d6571fa106 -r 23df3da5ffb5 src/ZF/Coind/BCR.thy
--- a/src/ZF/Coind/BCR.thy	Wed Mar 08 17:23:07 1995 +0100
+++ b/src/ZF/Coind/BCR.thy	Thu Mar 09 10:38:30 1995 +0100
@@ -6,22 +6,22 @@
 
 BCR = Values + Types +
 
-(* Basic correspondence relation *)
+(*Basic correspondence relation -- not completely specified, as it is a
+  parameter of the proof.  A concrete version could be defined inductively.*)
 
 consts
   isof :: "[i,i] => o"
 rules
   isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
 
-(* Extension to environments *)
+(*Its extension to environments*)
 
 consts
   isofenv :: "[i,i] => o"
-rules
-  isofenv_def "isofenv(ve,te) ==   \
-\   ve_dom(ve) = te_dom(te) &   \
-\   ( ALL x:ve_dom(ve).   \
+defs
+  isofenv_def "isofenv(ve,te) ==   		\
+\   ve_dom(ve) = te_dom(te) &   		\
+\   ( ALL x:ve_dom(ve).   			\
 \     EX c:Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
-
   
 end