src/ZF/ex/LList.ML
changeset 120 09287f26bfb8
parent 85 914270f33f2d
child 173 85071e6ad295
     1.1 --- a/src/ZF/ex/LList.ML	Mon Nov 15 14:33:40 1993 +0100
     1.2 +++ b/src/ZF/ex/LList.ML	Mon Nov 15 14:41:25 1993 +0100
     1.3 @@ -3,10 +3,10 @@
     1.4      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1993  University of Cambridge
     1.6  
     1.7 -Co-Datatype definition of Lazy Lists
     1.8 +CoDatatype definition of Lazy Lists
     1.9  *)
    1.10  
    1.11 -structure LList = Co_Datatype_Fun
    1.12 +structure LList = CoDatatype_Fun
    1.13   (val thy = QUniv.thy;
    1.14    val rec_specs = 
    1.15        [("llist", "quniv(A)",
    1.16 @@ -18,8 +18,8 @@
    1.17        ["LNil : llist(A)",
    1.18         "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
    1.19    val monos = [];
    1.20 -  val type_intrs = co_datatype_intrs
    1.21 -  val type_elims = co_datatype_elims);
    1.22 +  val type_intrs = codatatype_intrs
    1.23 +  val type_elims = codatatype_elims);
    1.24    
    1.25  val [LNilI, LConsI] = LList.intrs;
    1.26  
    1.27 @@ -46,7 +46,7 @@
    1.28    QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv];
    1.29  
    1.30  val quniv_cs = ZF_cs addSIs in_quniv_rls 
    1.31 -                     addIs (Int_quniv_in_quniv::co_datatype_intrs);
    1.32 +                     addIs (Int_quniv_in_quniv::codatatype_intrs);
    1.33  
    1.34  (*Keep unfolding the lazy list until the induction hypothesis applies*)
    1.35  goal LList.thy