Improved layout for inductive defs
authorlcp
Thu Mar 17 12:36:58 1994 +0100 (1994-03-17)
changeset 2797738aed3f84d
parent 278 523518f44286
child 280 fb379160f4de
Improved layout for inductive defs
src/ZF/List.ML
src/ZF/ex/Acc.ML
src/ZF/ex/Data.ML
src/ZF/ex/LList.ML
src/ZF/ex/LList_Eq.ML
src/ZF/ex/ListN.ML
src/ZF/ex/Primrec0.ML
src/ZF/ex/TF.ML
src/ZF/ex/acc.ML
src/ZF/ex/data.ML
src/ZF/ex/listn.ML
src/ZF/ex/llist.ML
src/ZF/ex/llist_eq.ML
src/ZF/ex/primrec0.ML
src/ZF/ex/tf.ML
src/ZF/fin.ML
src/ZF/list.ML
src/ZF/simpdata.ML
     1.1 --- a/src/ZF/List.ML	Thu Mar 17 11:24:31 1994 +0100
     1.2 +++ b/src/ZF/List.ML	Thu Mar 17 12:36:58 1994 +0100
     1.3 @@ -7,17 +7,15 @@
     1.4  *)
     1.5  
     1.6  structure List = Datatype_Fun
     1.7 - (val thy = Univ.thy;
     1.8 -  val rec_specs = 
     1.9 -      [("list", "univ(A)",
    1.10 -	  [(["Nil"],	"i"), 
    1.11 -	   (["Cons"],	"[i,i]=>i")])];
    1.12 -  val rec_styp = "i=>i";
    1.13 -  val ext = None
    1.14 -  val sintrs = 
    1.15 -      ["Nil : list(A)",
    1.16 -       "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
    1.17 -  val monos = [];
    1.18 + (val thy        = Univ.thy
    1.19 +  val rec_specs  = [("list", "univ(A)",
    1.20 +                      [(["Nil"],    "i"), 
    1.21 +                       (["Cons"],   "[i,i]=>i")])]
    1.22 +  val rec_styp   = "i=>i"
    1.23 +  val ext        = None
    1.24 +  val sintrs     = ["Nil : list(A)",
    1.25 +                    "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]
    1.26 +  val monos      = []
    1.27    val type_intrs = datatype_intrs
    1.28    val type_elims = datatype_elims);
    1.29  
     2.1 --- a/src/ZF/ex/Acc.ML	Thu Mar 17 11:24:31 1994 +0100
     2.2 +++ b/src/ZF/ex/Acc.ML	Thu Mar 17 12:36:58 1994 +0100
     2.3 @@ -10,13 +10,12 @@
     2.4  *)
     2.5  
     2.6  structure Acc = Inductive_Fun
     2.7 - (val thy = WF.thy addconsts [(["acc"],"i=>i")];
     2.8 -  val rec_doms = [("acc", "field(r)")];
     2.9 -  val sintrs = 
    2.10 -      ["[| r-``{a} : Pow(acc(r));  a : field(r) |] ==> a : acc(r)"];
    2.11 -  val monos = [Pow_mono];
    2.12 -  val con_defs = [];
    2.13 -  val type_intrs = [];
    2.14 + (val thy        = WF.thy addconsts [(["acc"],"i=>i")]
    2.15 +  val rec_doms   = [("acc", "field(r)")]
    2.16 +  val sintrs     = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
    2.17 +  val monos      = [Pow_mono]
    2.18 +  val con_defs   = []
    2.19 +  val type_intrs = []
    2.20    val type_elims = []);
    2.21  
    2.22  goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
     3.1 --- a/src/ZF/ex/Data.ML	Thu Mar 17 11:24:31 1994 +0100
     3.2 +++ b/src/ZF/ex/Data.ML	Thu Mar 17 12:36:58 1994 +0100
     3.3 @@ -8,21 +8,20 @@
     3.4  *)
     3.5  
     3.6  structure Data = Datatype_Fun
     3.7 - (val thy = Univ.thy;
     3.8 -  val rec_specs = 
     3.9 -      [("data", "univ(A Un B)",
    3.10 -	  [(["Con0"],	"i"),
    3.11 -	   (["Con1"],	"i=>i"),
    3.12 -	   (["Con2"],	"[i,i]=>i"),
    3.13 -	   (["Con3"],	"[i,i,i]=>i")])];
    3.14 -  val rec_styp = "[i,i]=>i";
    3.15 -  val ext = None
    3.16 -  val sintrs = 
    3.17 -	  ["Con0 : data(A,B)",
    3.18 -	   "[| a: A |] ==> Con1(a) : data(A,B)",
    3.19 -	   "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
    3.20 -	   "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];
    3.21 -  val monos = [];
    3.22 + (val thy        = Univ.thy
    3.23 +  val rec_specs  = [("data", "univ(A Un B)",
    3.24 +                       [(["Con0"],   "i"),
    3.25 +                        (["Con1"],   "i=>i"),
    3.26 +                        (["Con2"],   "[i,i]=>i"),
    3.27 +                        (["Con3"],   "[i,i,i]=>i")])]
    3.28 +  val rec_styp   = "[i,i]=>i"
    3.29 +  val ext        = None
    3.30 +  val sintrs     = 
    3.31 +          ["Con0 : data(A,B)",
    3.32 +           "[| a: A |] ==> Con1(a) : data(A,B)",
    3.33 +           "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
    3.34 +           "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]
    3.35 +  val monos      = []
    3.36    val type_intrs = datatype_intrs
    3.37    val type_elims = datatype_elims);
    3.38  
     4.1 --- a/src/ZF/ex/LList.ML	Thu Mar 17 11:24:31 1994 +0100
     4.2 +++ b/src/ZF/ex/LList.ML	Thu Mar 17 12:36:58 1994 +0100
     4.3 @@ -7,20 +7,18 @@
     4.4  *)
     4.5  
     4.6  structure LList = CoDatatype_Fun
     4.7 - (val thy = QUniv.thy;
     4.8 -  val rec_specs = 
     4.9 -      [("llist", "quniv(A)",
    4.10 -	  [(["LNil"],	"i"), 
    4.11 -	   (["LCons"],	"[i,i]=>i")])];
    4.12 -  val rec_styp = "i=>i";
    4.13 -  val ext = None
    4.14 -  val sintrs = 
    4.15 -      ["LNil : llist(A)",
    4.16 -       "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
    4.17 -  val monos = [];
    4.18 + (val thy        = QUniv.thy
    4.19 +  val rec_specs  = [("llist", "quniv(A)",
    4.20 +                      [(["LNil"],   "i"), 
    4.21 +                       (["LCons"],  "[i,i]=>i")])]
    4.22 +  val rec_styp   = "i=>i"
    4.23 +  val ext        = None
    4.24 +  val sintrs     = ["LNil : llist(A)",
    4.25 +                    "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"]
    4.26 +  val monos      = []
    4.27    val type_intrs = codatatype_intrs
    4.28    val type_elims = codatatype_elims);
    4.29 -  
    4.30 +
    4.31  val [LNilI, LConsI] = LList.intrs;
    4.32  
    4.33  (*An elimination rule, for type-checking*)
     5.1 --- a/src/ZF/ex/LList_Eq.ML	Thu Mar 17 11:24:31 1994 +0100
     5.2 +++ b/src/ZF/ex/LList_Eq.ML	Thu Mar 17 12:36:58 1994 +0100
     5.3 @@ -11,14 +11,14 @@
     5.4    a q/Q to the Sigma, Pair and converse rules.*)
     5.5  
     5.6  structure LList_Eq = CoInductive_Fun
     5.7 - (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
     5.8 -  val rec_doms = [("lleq", "llist(A) * llist(A)")];
     5.9 -  val sintrs = 
    5.10 -      ["<LNil, LNil> : lleq(A)",
    5.11 -       "[| a:A;  <l, l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')> : lleq(A)"];
    5.12 -  val monos = [];
    5.13 -  val con_defs = [];
    5.14 -  val type_intrs = LList.intrs@[SigmaI];
    5.15 + (val thy = LList.thy addconsts [(["lleq"],"i=>i")]
    5.16 +  val rec_doms   = [("lleq", "llist(A) * llist(A)")]
    5.17 +  val sintrs     = 
    5.18 +        ["<LNil, LNil> : lleq(A)",
    5.19 +         "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"]
    5.20 +  val monos      = []
    5.21 +  val con_defs   = []
    5.22 +  val type_intrs = LList.intrs @ [SigmaI]
    5.23    val type_elims = [SigmaE2]);
    5.24  
    5.25  (** Alternatives for above:
     6.1 --- a/src/ZF/ex/ListN.ML	Thu Mar 17 11:24:31 1994 +0100
     6.2 +++ b/src/ZF/ex/ListN.ML	Thu Mar 17 12:36:58 1994 +0100
     6.3 @@ -10,14 +10,14 @@
     6.4  *)
     6.5  
     6.6  structure ListN = Inductive_Fun
     6.7 - (val thy = ListFn.thy addconsts [(["listn"],"i=>i")];
     6.8 -  val rec_doms = [("listn", "nat*list(A)")];
     6.9 -  val sintrs = 
    6.10 -      ["<0,Nil> : listn(A)",
    6.11 -       "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"];
    6.12 -  val monos = [];
    6.13 -  val con_defs = [];
    6.14 -  val type_intrs = nat_typechecks@List.intrs@[SigmaI]
    6.15 + (val thy        = ListFn.thy addconsts [(["listn"],"i=>i")]
    6.16 +  val rec_doms   = [("listn", "nat*list(A)")]
    6.17 +  val sintrs     = 
    6.18 +          ["<0,Nil> : listn(A)",
    6.19 +           "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
    6.20 +  val monos      = []
    6.21 +  val con_defs   = []
    6.22 +  val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]
    6.23    val type_elims = [SigmaE2]);
    6.24  
    6.25  val listn_induct = standard 
     7.1 --- a/src/ZF/ex/Primrec0.ML	Thu Mar 17 11:24:31 1994 +0100
     7.2 +++ b/src/ZF/ex/Primrec0.ML	Thu Mar 17 12:36:58 1994 +0100
     7.3 @@ -64,20 +64,20 @@
     7.4  (*** Inductive definition of the PR functions ***)
     7.5  
     7.6  structure Primrec = Inductive_Fun
     7.7 - (val thy = Primrec0.thy;
     7.8 -  val rec_doms = [("primrec", "list(nat)->nat")];
     7.9 -  val ext = None
    7.10 -  val sintrs = 
    7.11 + (val thy        = Primrec0.thy
    7.12 +  val rec_doms   = [("primrec", "list(nat)->nat")]
    7.13 +  val sintrs     = 
    7.14        ["SC : primrec",
    7.15         "k: nat ==> CONST(k) : primrec",
    7.16         "i: nat ==> PROJ(i) : primrec",
    7.17 -       "[| g: primrec;  fs: list(primrec) |] ==> COMP(g,fs): primrec",
    7.18 -       "[| f: primrec;  g: primrec |] ==> PREC(f,g): primrec"];
    7.19 -  val monos = [list_mono];
    7.20 -  val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
    7.21 +       "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
    7.22 +       "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"]
    7.23 +  val monos      = [list_mono]
    7.24 +  val con_defs   = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]
    7.25    val type_intrs = pr0_typechecks
    7.26    val type_elims = []);
    7.27  
    7.28 +
    7.29  (* c: primrec ==> c: list(nat) -> nat *)
    7.30  val primrec_into_fun = Primrec.dom_subset RS subsetD;
    7.31  
     8.1 --- a/src/ZF/ex/TF.ML	Thu Mar 17 11:24:31 1994 +0100
     8.2 +++ b/src/ZF/ex/TF.ML	Thu Mar 17 12:36:58 1994 +0100
     8.3 @@ -7,20 +7,19 @@
     8.4  *)
     8.5  
     8.6  structure TF = Datatype_Fun
     8.7 - (val thy = Univ.thy;
     8.8 -  val rec_specs = 
     8.9 -      [("tree", "univ(A)",
    8.10 -	  [(["Tcons"],	"[i,i]=>i")]),
    8.11 -       ("forest", "univ(A)",
    8.12 -	  [(["Fnil"],	"i"),
    8.13 -	   (["Fcons"],	"[i,i]=>i")])];
    8.14 -  val rec_styp = "i=>i";
    8.15 -  val ext = None
    8.16 -  val sintrs = 
    8.17 -	  ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
    8.18 -	   "Fnil : forest(A)",
    8.19 -	   "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
    8.20 -  val monos = [];
    8.21 + (val thy        = Univ.thy
    8.22 +  val rec_specs  = [("tree", "univ(A)",
    8.23 +                       [(["Tcons"],  "[i,i]=>i")]),
    8.24 +                    ("forest", "univ(A)",
    8.25 +                       [(["Fnil"],   "i"),
    8.26 +                        (["Fcons"],  "[i,i]=>i")])]
    8.27 +  val rec_styp   = "i=>i"
    8.28 +  val ext        = None
    8.29 +  val sintrs     = 
    8.30 +          ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
    8.31 +           "Fnil : forest(A)",
    8.32 +           "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"]
    8.33 +  val monos      = []
    8.34    val type_intrs = datatype_intrs
    8.35    val type_elims = datatype_elims);
    8.36  
     9.1 --- a/src/ZF/ex/acc.ML	Thu Mar 17 11:24:31 1994 +0100
     9.2 +++ b/src/ZF/ex/acc.ML	Thu Mar 17 12:36:58 1994 +0100
     9.3 @@ -10,13 +10,12 @@
     9.4  *)
     9.5  
     9.6  structure Acc = Inductive_Fun
     9.7 - (val thy = WF.thy addconsts [(["acc"],"i=>i")];
     9.8 -  val rec_doms = [("acc", "field(r)")];
     9.9 -  val sintrs = 
    9.10 -      ["[| r-``{a} : Pow(acc(r));  a : field(r) |] ==> a : acc(r)"];
    9.11 -  val monos = [Pow_mono];
    9.12 -  val con_defs = [];
    9.13 -  val type_intrs = [];
    9.14 + (val thy        = WF.thy addconsts [(["acc"],"i=>i")]
    9.15 +  val rec_doms   = [("acc", "field(r)")]
    9.16 +  val sintrs     = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
    9.17 +  val monos      = [Pow_mono]
    9.18 +  val con_defs   = []
    9.19 +  val type_intrs = []
    9.20    val type_elims = []);
    9.21  
    9.22  goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
    10.1 --- a/src/ZF/ex/data.ML	Thu Mar 17 11:24:31 1994 +0100
    10.2 +++ b/src/ZF/ex/data.ML	Thu Mar 17 12:36:58 1994 +0100
    10.3 @@ -8,21 +8,20 @@
    10.4  *)
    10.5  
    10.6  structure Data = Datatype_Fun
    10.7 - (val thy = Univ.thy;
    10.8 -  val rec_specs = 
    10.9 -      [("data", "univ(A Un B)",
   10.10 -	  [(["Con0"],	"i"),
   10.11 -	   (["Con1"],	"i=>i"),
   10.12 -	   (["Con2"],	"[i,i]=>i"),
   10.13 -	   (["Con3"],	"[i,i,i]=>i")])];
   10.14 -  val rec_styp = "[i,i]=>i";
   10.15 -  val ext = None
   10.16 -  val sintrs = 
   10.17 -	  ["Con0 : data(A,B)",
   10.18 -	   "[| a: A |] ==> Con1(a) : data(A,B)",
   10.19 -	   "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
   10.20 -	   "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"];
   10.21 -  val monos = [];
   10.22 + (val thy        = Univ.thy
   10.23 +  val rec_specs  = [("data", "univ(A Un B)",
   10.24 +                       [(["Con0"],   "i"),
   10.25 +                        (["Con1"],   "i=>i"),
   10.26 +                        (["Con2"],   "[i,i]=>i"),
   10.27 +                        (["Con3"],   "[i,i,i]=>i")])]
   10.28 +  val rec_styp   = "[i,i]=>i"
   10.29 +  val ext        = None
   10.30 +  val sintrs     = 
   10.31 +          ["Con0 : data(A,B)",
   10.32 +           "[| a: A |] ==> Con1(a) : data(A,B)",
   10.33 +           "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
   10.34 +           "[| a: A; b: B;  d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]
   10.35 +  val monos      = []
   10.36    val type_intrs = datatype_intrs
   10.37    val type_elims = datatype_elims);
   10.38  
    11.1 --- a/src/ZF/ex/listn.ML	Thu Mar 17 11:24:31 1994 +0100
    11.2 +++ b/src/ZF/ex/listn.ML	Thu Mar 17 12:36:58 1994 +0100
    11.3 @@ -10,14 +10,14 @@
    11.4  *)
    11.5  
    11.6  structure ListN = Inductive_Fun
    11.7 - (val thy = ListFn.thy addconsts [(["listn"],"i=>i")];
    11.8 -  val rec_doms = [("listn", "nat*list(A)")];
    11.9 -  val sintrs = 
   11.10 -      ["<0,Nil> : listn(A)",
   11.11 -       "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"];
   11.12 -  val monos = [];
   11.13 -  val con_defs = [];
   11.14 -  val type_intrs = nat_typechecks@List.intrs@[SigmaI]
   11.15 + (val thy        = ListFn.thy addconsts [(["listn"],"i=>i")]
   11.16 +  val rec_doms   = [("listn", "nat*list(A)")]
   11.17 +  val sintrs     = 
   11.18 +          ["<0,Nil> : listn(A)",
   11.19 +           "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
   11.20 +  val monos      = []
   11.21 +  val con_defs   = []
   11.22 +  val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]
   11.23    val type_elims = [SigmaE2]);
   11.24  
   11.25  val listn_induct = standard 
    12.1 --- a/src/ZF/ex/llist.ML	Thu Mar 17 11:24:31 1994 +0100
    12.2 +++ b/src/ZF/ex/llist.ML	Thu Mar 17 12:36:58 1994 +0100
    12.3 @@ -7,20 +7,18 @@
    12.4  *)
    12.5  
    12.6  structure LList = CoDatatype_Fun
    12.7 - (val thy = QUniv.thy;
    12.8 -  val rec_specs = 
    12.9 -      [("llist", "quniv(A)",
   12.10 -	  [(["LNil"],	"i"), 
   12.11 -	   (["LCons"],	"[i,i]=>i")])];
   12.12 -  val rec_styp = "i=>i";
   12.13 -  val ext = None
   12.14 -  val sintrs = 
   12.15 -      ["LNil : llist(A)",
   12.16 -       "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"];
   12.17 -  val monos = [];
   12.18 + (val thy        = QUniv.thy
   12.19 +  val rec_specs  = [("llist", "quniv(A)",
   12.20 +                      [(["LNil"],   "i"), 
   12.21 +                       (["LCons"],  "[i,i]=>i")])]
   12.22 +  val rec_styp   = "i=>i"
   12.23 +  val ext        = None
   12.24 +  val sintrs     = ["LNil : llist(A)",
   12.25 +                    "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"]
   12.26 +  val monos      = []
   12.27    val type_intrs = codatatype_intrs
   12.28    val type_elims = codatatype_elims);
   12.29 -  
   12.30 +
   12.31  val [LNilI, LConsI] = LList.intrs;
   12.32  
   12.33  (*An elimination rule, for type-checking*)
    13.1 --- a/src/ZF/ex/llist_eq.ML	Thu Mar 17 11:24:31 1994 +0100
    13.2 +++ b/src/ZF/ex/llist_eq.ML	Thu Mar 17 12:36:58 1994 +0100
    13.3 @@ -11,14 +11,14 @@
    13.4    a q/Q to the Sigma, Pair and converse rules.*)
    13.5  
    13.6  structure LList_Eq = CoInductive_Fun
    13.7 - (val thy = LList.thy addconsts [(["lleq"],"i=>i")];
    13.8 -  val rec_doms = [("lleq", "llist(A) * llist(A)")];
    13.9 -  val sintrs = 
   13.10 -      ["<LNil, LNil> : lleq(A)",
   13.11 -       "[| a:A;  <l, l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')> : lleq(A)"];
   13.12 -  val monos = [];
   13.13 -  val con_defs = [];
   13.14 -  val type_intrs = LList.intrs@[SigmaI];
   13.15 + (val thy = LList.thy addconsts [(["lleq"],"i=>i")]
   13.16 +  val rec_doms   = [("lleq", "llist(A) * llist(A)")]
   13.17 +  val sintrs     = 
   13.18 +        ["<LNil, LNil> : lleq(A)",
   13.19 +         "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"]
   13.20 +  val monos      = []
   13.21 +  val con_defs   = []
   13.22 +  val type_intrs = LList.intrs @ [SigmaI]
   13.23    val type_elims = [SigmaE2]);
   13.24  
   13.25  (** Alternatives for above:
    14.1 --- a/src/ZF/ex/primrec0.ML	Thu Mar 17 11:24:31 1994 +0100
    14.2 +++ b/src/ZF/ex/primrec0.ML	Thu Mar 17 12:36:58 1994 +0100
    14.3 @@ -64,20 +64,20 @@
    14.4  (*** Inductive definition of the PR functions ***)
    14.5  
    14.6  structure Primrec = Inductive_Fun
    14.7 - (val thy = Primrec0.thy;
    14.8 -  val rec_doms = [("primrec", "list(nat)->nat")];
    14.9 -  val ext = None
   14.10 -  val sintrs = 
   14.11 + (val thy        = Primrec0.thy
   14.12 +  val rec_doms   = [("primrec", "list(nat)->nat")]
   14.13 +  val sintrs     = 
   14.14        ["SC : primrec",
   14.15         "k: nat ==> CONST(k) : primrec",
   14.16         "i: nat ==> PROJ(i) : primrec",
   14.17 -       "[| g: primrec;  fs: list(primrec) |] ==> COMP(g,fs): primrec",
   14.18 -       "[| f: primrec;  g: primrec |] ==> PREC(f,g): primrec"];
   14.19 -  val monos = [list_mono];
   14.20 -  val con_defs = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def];
   14.21 +       "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
   14.22 +       "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"]
   14.23 +  val monos      = [list_mono]
   14.24 +  val con_defs   = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]
   14.25    val type_intrs = pr0_typechecks
   14.26    val type_elims = []);
   14.27  
   14.28 +
   14.29  (* c: primrec ==> c: list(nat) -> nat *)
   14.30  val primrec_into_fun = Primrec.dom_subset RS subsetD;
   14.31  
    15.1 --- a/src/ZF/ex/tf.ML	Thu Mar 17 11:24:31 1994 +0100
    15.2 +++ b/src/ZF/ex/tf.ML	Thu Mar 17 12:36:58 1994 +0100
    15.3 @@ -7,20 +7,19 @@
    15.4  *)
    15.5  
    15.6  structure TF = Datatype_Fun
    15.7 - (val thy = Univ.thy;
    15.8 -  val rec_specs = 
    15.9 -      [("tree", "univ(A)",
   15.10 -	  [(["Tcons"],	"[i,i]=>i")]),
   15.11 -       ("forest", "univ(A)",
   15.12 -	  [(["Fnil"],	"i"),
   15.13 -	   (["Fcons"],	"[i,i]=>i")])];
   15.14 -  val rec_styp = "i=>i";
   15.15 -  val ext = None
   15.16 -  val sintrs = 
   15.17 -	  ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
   15.18 -	   "Fnil : forest(A)",
   15.19 -	   "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"];
   15.20 -  val monos = [];
   15.21 + (val thy        = Univ.thy
   15.22 +  val rec_specs  = [("tree", "univ(A)",
   15.23 +                       [(["Tcons"],  "[i,i]=>i")]),
   15.24 +                    ("forest", "univ(A)",
   15.25 +                       [(["Fnil"],   "i"),
   15.26 +                        (["Fcons"],  "[i,i]=>i")])]
   15.27 +  val rec_styp   = "i=>i"
   15.28 +  val ext        = None
   15.29 +  val sintrs     = 
   15.30 +          ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
   15.31 +           "Fnil : forest(A)",
   15.32 +           "[| t: tree(A);  f: forest(A) |] ==> Fcons(t,f) : forest(A)"]
   15.33 +  val monos      = []
   15.34    val type_intrs = datatype_intrs
   15.35    val type_elims = datatype_elims);
   15.36  
    16.1 --- a/src/ZF/fin.ML	Thu Mar 17 11:24:31 1994 +0100
    16.2 +++ b/src/ZF/fin.ML	Thu Mar 17 12:36:58 1994 +0100
    16.3 @@ -18,13 +18,12 @@
    16.4  *)
    16.5  
    16.6  structure Fin = Inductive_Fun
    16.7 - (val thy = Arith.thy addconsts [(["Fin"],"i=>i")];
    16.8 -  val rec_doms = [("Fin","Pow(A)")];
    16.9 -  val sintrs = 
   16.10 -	  ["0 : Fin(A)",
   16.11 -	   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"];
   16.12 -  val monos = [];
   16.13 -  val con_defs = [];
   16.14 + (val thy        = Arith.thy addconsts [(["Fin"],"i=>i")]
   16.15 +  val rec_doms   = [("Fin","Pow(A)")]
   16.16 +  val sintrs     = ["0 : Fin(A)",
   16.17 +                    "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
   16.18 +  val monos      = []
   16.19 +  val con_defs   = []
   16.20    val type_intrs = [empty_subsetI, cons_subsetI, PowI]
   16.21    val type_elims = [make_elim PowD]);
   16.22  
    17.1 --- a/src/ZF/list.ML	Thu Mar 17 11:24:31 1994 +0100
    17.2 +++ b/src/ZF/list.ML	Thu Mar 17 12:36:58 1994 +0100
    17.3 @@ -7,17 +7,15 @@
    17.4  *)
    17.5  
    17.6  structure List = Datatype_Fun
    17.7 - (val thy = Univ.thy;
    17.8 -  val rec_specs = 
    17.9 -      [("list", "univ(A)",
   17.10 -	  [(["Nil"],	"i"), 
   17.11 -	   (["Cons"],	"[i,i]=>i")])];
   17.12 -  val rec_styp = "i=>i";
   17.13 -  val ext = None
   17.14 -  val sintrs = 
   17.15 -      ["Nil : list(A)",
   17.16 -       "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
   17.17 -  val monos = [];
   17.18 + (val thy        = Univ.thy
   17.19 +  val rec_specs  = [("list", "univ(A)",
   17.20 +                      [(["Nil"],    "i"), 
   17.21 +                       (["Cons"],   "[i,i]=>i")])]
   17.22 +  val rec_styp   = "i=>i"
   17.23 +  val ext        = None
   17.24 +  val sintrs     = ["Nil : list(A)",
   17.25 +                    "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]
   17.26 +  val monos      = []
   17.27    val type_intrs = datatype_intrs
   17.28    val type_elims = datatype_elims);
   17.29  
    18.1 --- a/src/ZF/simpdata.ML	Thu Mar 17 11:24:31 1994 +0100
    18.2 +++ b/src/ZF/simpdata.ML	Thu Mar 17 12:36:58 1994 +0100
    18.3 @@ -86,9 +86,6 @@
    18.4        | _ $ A => tryrules atomize_pairs A
    18.5    end;
    18.6  
    18.7 -fun ZF_mk_rew_rules th = map mk_meta_eq (atomize th);
    18.8 -
    18.9 -
   18.10  val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
   18.11  		beta, eta, restrict, fst_conv, snd_conv, split];
   18.12  
   18.13 @@ -99,6 +96,6 @@
   18.14     [ball_cong, bex_cong, Replace_cong, RepFun_cong, Collect_cong, lam_cong];
   18.15  
   18.16  val ZF_ss = FOL_ss 
   18.17 -      setmksimps ZF_mk_rew_rules
   18.18 +      setmksimps (map mk_meta_eq o atomize o gen_all)
   18.19        addsimps (ZF_simps @ mem_simps @ bquant_simps)
   18.20        addcongs ZF_congs;