src/ZF/Coind/BCR.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Coind/BCR.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Coind/BCR.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -10,14 +10,14 @@
     1.4    parameter of the proof.  A concrete version could be defined inductively.*)
     1.5  
     1.6  consts
     1.7 -  isof :: "[i,i] => o"
     1.8 +  isof :: [i,i] => o
     1.9  rules
    1.10    isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
    1.11  
    1.12  (*Its extension to environments*)
    1.13  
    1.14  consts
    1.15 -  isofenv :: "[i,i] => o"
    1.16 +  isofenv :: [i,i] => o
    1.17  defs
    1.18    isofenv_def "isofenv(ve,te) ==   		
    1.19     ve_dom(ve) = te_dom(te) &