src/ZF/Coind/BCR.thy

--- a/src/ZF/Coind/BCR.thy	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/BCR.thy	Tue Dec 25 10:02:01 2001 +0100
@@ -3,25 +3,3 @@
     Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 *)
-
-BCR = Values + Types +
-
-(*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)"
-
-(*Its extension to environments*)
-
-consts
-  isofenv :: [i,i] => o
-defs
-  isofenv_def "isofenv(ve,te) ==                
-   ve_dom(ve) = te_dom(te) &            
-   ( \\<forall>x \\<in> ve_dom(ve).                          
-     \\<exists>c \\<in> Const. ve_app(ve,x) = v_const(c) & isof(c,te_app(te,x)))"
-  
-end