src/ZF/Coind/Static.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Coind/Static.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Coind/Static.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  Static = BCR +
     1.5  
     1.6  consts
     1.7 -  ElabRel :: "i"
     1.8 +  ElabRel :: i
     1.9  inductive
    1.10    domains "ElabRel" <= "TyEnv * Exp * Ty"
    1.11    intrs