--- a/src/ZF/List.thy Mon Dec 19 15:22:42 1994 +0100 +++ b/src/ZF/List.thy Mon Dec 19 15:30:30 1994 +0100 @@ -10,7 +10,7 @@ although complicating its derivation. *) -List = "Datatype" + Univ + +List = Datatype + consts "@" :: "[i,i]=>i" (infixr 60)