1.1 --- a/src/ZF/ex/Data.ML	Thu Oct 28 11:30:35 1993 +0100
     1.2 +++ b/src/ZF/ex/Data.ML	Thu Oct 28 11:32:37 1993 +0100
     1.3 @@ -11,17 +11,17 @@
     1.4   (val thy = Univ.thy;
     1.5    val rec_specs = 
     1.6        [("data", "univ(A Un B)",
     1.7 -	  [(["Zero"],	"i"),
     1.8 -	   (["One"],	"i=>i"),
     1.9 -	   (["Two"],	"[i,i]=>i"),
    1.10 -	   (["Three"],	"[i,i,i]=>i")])];
    1.11 +	  [(["Con0"],	"i"),
    1.12 +	   (["Con1"],	"i=>i"),
    1.13 +	   (["Con2"],	"[i,i]=>i"),
    1.14 +	   (["Con3"],	"[i,i,i]=>i")])];
    1.15    val rec_styp = "[i,i]=>i";
    1.16    val ext = None
    1.17    val sintrs = 
    1.18 -	  ["Zero : data(A,B)",
    1.19 -	   "[| a: A |] ==> One(a) : data(A,B)",
    1.20 -	   "[| a: A; b: B |] ==> Two(a,b) : data(A,B)",
    1.21 -	   "[| a: A; b: B;  d: data(A,B) |] ==> Three(a,b,d) : data(A,B)"];
    1.22 +	  ["Con0 : data(A,B)",
    1.23 +	   "[| a: A |] ==> Con1(a) : data(A,B)",
    1.24 +	   "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
    1.25 +	   "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];
    1.26    val monos = [];
    1.27    val type_intrs = datatype_intrs
    1.28    val type_elims = datatype_elims);

     2.1 --- a/src/ZF/ex/LList.ML	Thu Oct 28 11:30:35 1993 +0100
     2.2 +++ b/src/ZF/ex/LList.ML	Thu Oct 28 11:32:37 1993 +0100
     2.3 @@ -4,9 +4,6 @@
     2.4      Copyright   1993  University of Cambridge
     2.5  
     2.6  Co-Datatype definition of Lazy Lists
     2.7 -
     2.8 -Needs a "take-lemma" to prove llist_subset_quniv and to justify co-induction
     2.9 -for proving equality
    2.10  *)
    2.11  
    2.12  structure LList = Co_Datatype_Fun
    2.13 @@ -22,7 +19,7 @@
    2.14         "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
    2.15    val monos = [];
    2.16    val type_intrs = co_datatype_intrs
    2.17 -  val type_elims = []);
    2.18 +  val type_elims = co_datatype_elims);
    2.19    
    2.20  val [LNilI, LConsI] = LList.intrs;
    2.21  

     3.1 --- a/src/ZF/ex/ListN.ML	Thu Oct 28 11:30:35 1993 +0100
     3.2 +++ b/src/ZF/ex/ListN.ML	Thu Oct 28 11:32:37 1993 +0100
     3.3 @@ -55,4 +55,7 @@
     3.4  val listn_append = result();
     3.5  
     3.6  val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)"
     3.7 -and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,xs)> : listn(A)";
     3.8 +and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,l)> : listn(A)";
     3.9 +
    3.10 +val zero_listn_case = ListN.mk_cases List.con_defs "<0,l> : listn(A)"
    3.11 +and succ_listn_case = ListN.mk_cases List.con_defs "<succ(i),l> : listn(A)";

     4.1 --- a/src/ZF/ex/data.ML	Thu Oct 28 11:30:35 1993 +0100
     4.2 +++ b/src/ZF/ex/data.ML	Thu Oct 28 11:32:37 1993 +0100
     4.3 @@ -11,17 +11,17 @@
     4.4   (val thy = Univ.thy;
     4.5    val rec_specs = 
     4.6        [("data", "univ(A Un B)",
     4.7 -	  [(["Zero"],	"i"),
     4.8 -	   (["One"],	"i=>i"),
     4.9 -	   (["Two"],	"[i,i]=>i"),
    4.10 -	   (["Three"],	"[i,i,i]=>i")])];
    4.11 +	  [(["Con0"],	"i"),
    4.12 +	   (["Con1"],	"i=>i"),
    4.13 +	   (["Con2"],	"[i,i]=>i"),
    4.14 +	   (["Con3"],	"[i,i,i]=>i")])];
    4.15    val rec_styp = "[i,i]=>i";
    4.16    val ext = None
    4.17    val sintrs = 
    4.18 -	  ["Zero : data(A,B)",
    4.19 -	   "[| a: A |] ==> One(a) : data(A,B)",
    4.20 -	   "[| a: A; b: B |] ==> Two(a,b) : data(A,B)",
    4.21 -	   "[| a: A; b: B;  d: data(A,B) |] ==> Three(a,b,d) : data(A,B)"];
    4.22 +	  ["Con0 : data(A,B)",
    4.23 +	   "[| a: A |] ==> Con1(a) : data(A,B)",
    4.24 +	   "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
    4.25 +	   "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];
    4.26    val monos = [];
    4.27    val type_intrs = datatype_intrs
    4.28    val type_elims = datatype_elims);

     5.1 --- a/src/ZF/ex/listn.ML	Thu Oct 28 11:30:35 1993 +0100
     5.2 +++ b/src/ZF/ex/listn.ML	Thu Oct 28 11:32:37 1993 +0100
     5.3 @@ -55,4 +55,7 @@
     5.4  val listn_append = result();
     5.5  
     5.6  val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)"
     5.7 -and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,xs)> : listn(A)";
     5.8 +and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,l)> : listn(A)";
     5.9 +
    5.10 +val zero_listn_case = ListN.mk_cases List.con_defs "<0,l> : listn(A)"
    5.11 +and succ_listn_case = ListN.mk_cases List.con_defs "<succ(i),l> : listn(A)";

     6.1 --- a/src/ZF/ex/llist.ML	Thu Oct 28 11:30:35 1993 +0100
     6.2 +++ b/src/ZF/ex/llist.ML	Thu Oct 28 11:32:37 1993 +0100
     6.3 @@ -4,9 +4,6 @@
     6.4      Copyright   1993  University of Cambridge
     6.5  
     6.6  Co-Datatype definition of Lazy Lists
     6.7 -
     6.8 -Needs a "take-lemma" to prove llist_subset_quniv and to justify co-induction
     6.9 -for proving equality
    6.10  *)
    6.11  
    6.12  structure LList = Co_Datatype_Fun
    6.13 @@ -22,7 +19,7 @@
    6.14         "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
    6.15    val monos = [];
    6.16    val type_intrs = co_datatype_intrs
    6.17 -  val type_elims = []);
    6.18 +  val type_elims = co_datatype_elims);
    6.19    
    6.20  val [LNilI, LConsI] = LList.intrs;
    6.21