src/ZF/ex/Term.thy
changeset 6117 f9aad8ccd590
parent 6112 5e4871c5136b
child 6159 833b76d0e6dc
     1.1 --- a/src/ZF/ex/Term.thy	Wed Jan 13 12:44:33 1999 +0100
     1.2 +++ b/src/ZF/ex/Term.thy	Wed Jan 13 15:14:47 1999 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  datatype
     1.6    "term(A)" = Apply ("a: A", "l: list(term(A))")
     1.7 -  monos       "[list_mono]"
     1.8 +  monos        list_mono
     1.9  
    1.10    type_elims  "[make_elim (list_univ RS subsetD)]"
    1.11  (*Or could have