--- 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