src/ZF/List.ML
changeset 444 3ca9d49fd662
parent 435 ca5356bd315a
child 477 53fc8ad84b33
     1.1 --- a/src/ZF/List.ML	Wed Jun 29 12:13:03 1994 +0200
     1.2 +++ b/src/ZF/List.ML	Fri Jul 01 11:03:42 1994 +0200
     1.3 @@ -9,10 +9,9 @@
     1.4  structure List = Datatype_Fun
     1.5   (val thy        = Univ.thy
     1.6    val rec_specs  = [("list", "univ(A)",
     1.7 -                      [(["Nil"],    "i"), 
     1.8 -                       (["Cons"],   "[i,i]=>i")])]
     1.9 +                      [(["Nil"],    "i", NoSyn), 
    1.10 +                       (["Cons"],   "[i,i]=>i", NoSyn)])]
    1.11    val rec_styp   = "i=>i"
    1.12 -  val ext        = None
    1.13    val sintrs     = ["Nil : list(A)",
    1.14                      "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]
    1.15    val monos      = []