changed syntax of datatype declaration
authorclasohm
Fri Jul 01 11:04:12 1994 +0200 (1994-07-01 ago)
changeset 4457b6d8b8d4580
parent 444 3ca9d49fd662
child 446 3ee5c9314efe
changed syntax of datatype declaration
src/ZF/ex/Acc.ML
src/ZF/ex/BT.ML
src/ZF/ex/Bin.ML
src/ZF/ex/CoUnit.ML
src/ZF/ex/Comb.ML
src/ZF/ex/Data.ML
src/ZF/ex/Enum.ML
src/ZF/ex/LList.ML
src/ZF/ex/LList_Eq.ML
src/ZF/ex/ListN.ML
src/ZF/ex/Prop.ML
src/ZF/ex/Rmap.ML
src/ZF/ex/TF.ML
src/ZF/ex/Term.ML
     1.1 --- a/src/ZF/ex/Acc.ML	Fri Jul 01 11:03:42 1994 +0200
     1.2 +++ b/src/ZF/ex/Acc.ML	Fri Jul 01 11:04:12 1994 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  *)
     1.5  
     1.6  structure Acc = Inductive_Fun
     1.7 - (val thy        = WF.thy addconsts [(["acc"],"i=>i")]
     1.8 + (val thy        = WF.thy |> add_consts [("acc","i=>i",NoSyn)]
     1.9    val rec_doms   = [("acc", "field(r)")]
    1.10    val sintrs     = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
    1.11    val monos      = [Pow_mono]
     2.1 --- a/src/ZF/ex/BT.ML	Fri Jul 01 11:03:42 1994 +0200
     2.2 +++ b/src/ZF/ex/BT.ML	Fri Jul 01 11:04:12 1994 +0200
     2.3 @@ -10,9 +10,9 @@
     2.4   (val thy = Univ.thy;
     2.5    val rec_specs = 
     2.6        [("bt", "univ(A)",
     2.7 -	  [(["Lf"],"i"), (["Br"],"[i,i,i]=>i")])];
     2.8 +	  [(["Lf"],"i",NoSyn), 
     2.9 +           (["Br"],"[i,i,i]=>i", NoSyn)])];
    2.10    val rec_styp = "i=>i";
    2.11 -  val ext = None
    2.12    val sintrs = 
    2.13  	  ["Lf : bt(A)",
    2.14  	   "[| a: A;  t1: bt(A);  t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
     3.1 --- a/src/ZF/ex/Bin.ML	Fri Jul 01 11:03:42 1994 +0200
     3.2 +++ b/src/ZF/ex/Bin.ML	Fri Jul 01 11:04:12 1994 +0200
     3.3 @@ -11,11 +11,9 @@
     3.4   (val thy = Univ.thy;
     3.5    val rec_specs = 
     3.6        [("bin", "univ(0)",
     3.7 -	  [(["Plus", "Minus"],	"i"),
     3.8 -	   (["op $$"],		"[i,i]=>i")])];
     3.9 +	  [(["Plus", "Minus"],	"i", NoSyn),
    3.10 +	   (["$$"],		"[i,i]=>i", Infixl 60)])];
    3.11    val rec_styp = "i";
    3.12 -  val ext = Some (Syntax.simple_sext
    3.13 -		  [OldMixfix.Infixl("$$", "[i,i] => i", 60)]);
    3.14    val sintrs = 
    3.15  	  ["Plus : bin",
    3.16  	   "Minus : bin",
     4.1 --- a/src/ZF/ex/CoUnit.ML	Fri Jul 01 11:03:42 1994 +0200
     4.2 +++ b/src/ZF/ex/CoUnit.ML	Fri Jul 01 11:04:12 1994 +0200
     4.3 @@ -16,9 +16,8 @@
     4.4   (val thy = QUniv.thy;
     4.5    val rec_specs = 
     4.6        [("counit", "quniv(0)",
     4.7 -	  [(["Con"],	"i=>i")])];
     4.8 +	  [(["Con"],	"i=>i", NoSyn)])];
     4.9    val rec_styp = "i";
    4.10 -  val ext = None
    4.11    val sintrs = ["x: counit ==> Con(x) : counit"];
    4.12    val monos = [];
    4.13    val type_intrs = codatatype_intrs
    4.14 @@ -53,9 +52,8 @@
    4.15   (val thy = QUniv.thy;
    4.16    val rec_specs = 
    4.17        [("counit2", "quniv(0)",
    4.18 -	  [(["Con2"],	"[i,i]=>i")])];
    4.19 +	  [(["Con2"],	"[i,i]=>i", NoSyn)])];
    4.20    val rec_styp = "i";
    4.21 -  val ext = None
    4.22    val sintrs = ["[| x: counit2;  y: counit2 |] ==> Con2(x,y) : counit2"];
    4.23    val monos = [];
    4.24    val type_intrs = codatatype_intrs
     5.1 --- a/src/ZF/ex/Comb.ML	Fri Jul 01 11:03:42 1994 +0200
     5.2 +++ b/src/ZF/ex/Comb.ML	Fri Jul 01 11:04:12 1994 +0200
     5.3 @@ -16,11 +16,9 @@
     5.4   (val thy = Univ.thy;
     5.5    val rec_specs = 
     5.6        [("comb", "univ(0)",
     5.7 -	  [(["K","S"],	"i"),
     5.8 -	   (["op #"],	"[i,i]=>i")])];
     5.9 +	  [(["K","S"],	"i", NoSyn),
    5.10 +	   (["#"],	"[i,i]=>i", Infixl 90)])];
    5.11    val rec_styp = "i";
    5.12 -  val ext = Some (Syntax.simple_sext
    5.13 -		  [OldMixfix.Infixl("#", "[i,i] => i", 90)]);
    5.14    val sintrs = 
    5.15  	  ["K : comb",
    5.16  	   "S : comb",
     6.1 --- a/src/ZF/ex/Data.ML	Fri Jul 01 11:03:42 1994 +0200
     6.2 +++ b/src/ZF/ex/Data.ML	Fri Jul 01 11:04:12 1994 +0200
     6.3 @@ -10,12 +10,11 @@
     6.4  structure Data = Datatype_Fun
     6.5   (val thy        = Univ.thy
     6.6    val rec_specs  = [("data", "univ(A Un B)",
     6.7 -                       [(["Con0"],   "i"),
     6.8 -                        (["Con1"],   "i=>i"),
     6.9 -                        (["Con2"],   "[i,i]=>i"),
    6.10 -                        (["Con3"],   "[i,i,i]=>i")])]
    6.11 +                       [(["Con0"],   "i",NoSyn),
    6.12 +                        (["Con1"],   "i=>i",NoSyn),
    6.13 +                        (["Con2"],   "[i,i]=>i",NoSyn),
    6.14 +                        (["Con3"],   "[i,i,i]=>i",NoSyn)])]
    6.15    val rec_styp   = "[i,i]=>i"
    6.16 -  val ext        = None
    6.17    val sintrs     = 
    6.18            ["Con0 : data(A,B)",
    6.19             "[| a: A |] ==> Con1(a) : data(A,B)",
     7.1 --- a/src/ZF/ex/Enum.ML	Fri Jul 01 11:03:42 1994 +0200
     7.2 +++ b/src/ZF/ex/Enum.ML	Fri Jul 01 11:04:12 1994 +0200
     7.3 @@ -19,9 +19,8 @@
     7.4   (val thy = Univ.thy;
     7.5    val rec_specs = 
     7.6        [("enum", "univ(0)",
     7.7 -	  [(consts, "i")])];
     7.8 +	  [(consts, "i", NoSyn)])];
     7.9    val rec_styp = "i";
    7.10 -  val ext = None
    7.11    val sintrs = map (fn const => const ^ " : enum") consts;
    7.12    val monos = [];
    7.13    val type_intrs = datatype_intrs
     8.1 --- a/src/ZF/ex/LList.ML	Fri Jul 01 11:03:42 1994 +0200
     8.2 +++ b/src/ZF/ex/LList.ML	Fri Jul 01 11:04:12 1994 +0200
     8.3 @@ -9,10 +9,9 @@
     8.4  structure LList = CoDatatype_Fun
     8.5   (val thy        = QUniv.thy
     8.6    val rec_specs  = [("llist", "quniv(A)",
     8.7 -                      [(["LNil"],   "i"), 
     8.8 -                       (["LCons"],  "[i,i]=>i")])]
     8.9 +                      [(["LNil"],   "i",NoSyn), 
    8.10 +                       (["LCons"],  "[i,i]=>i",NoSyn)])]
    8.11    val rec_styp   = "i=>i"
    8.12 -  val ext        = None
    8.13    val sintrs     = ["LNil : llist(A)",
    8.14                      "[| a: A;  l: llist(A) |] ==> LCons(a,l) : llist(A)"]
    8.15    val monos      = []
     9.1 --- a/src/ZF/ex/LList_Eq.ML	Fri Jul 01 11:03:42 1994 +0200
     9.2 +++ b/src/ZF/ex/LList_Eq.ML	Fri Jul 01 11:04:12 1994 +0200
     9.3 @@ -11,7 +11,7 @@
     9.4    a q/Q to the Sigma, Pair and converse rules.*)
     9.5  
     9.6  structure LList_Eq = CoInductive_Fun
     9.7 - (val thy = LList.thy addconsts [(["lleq"],"i=>i")]
     9.8 + (val thy = LList.thy |> add_consts [("lleq","i=>i",NoSyn)]
     9.9    val rec_doms   = [("lleq", "llist(A) * llist(A)")]
    9.10    val sintrs     = 
    9.11          ["<LNil, LNil> : lleq(A)",
    10.1 --- a/src/ZF/ex/ListN.ML	Fri Jul 01 11:03:42 1994 +0200
    10.2 +++ b/src/ZF/ex/ListN.ML	Fri Jul 01 11:04:12 1994 +0200
    10.3 @@ -10,7 +10,7 @@
    10.4  *)
    10.5  
    10.6  structure ListN = Inductive_Fun
    10.7 - (val thy        = ListFn.thy addconsts [(["listn"],"i=>i")]
    10.8 + (val thy        = ListFn.thy |> add_consts [("listn","i=>i",NoSyn)]
    10.9    val rec_doms   = [("listn", "nat*list(A)")]
   10.10    val sintrs     = 
   10.11            ["<0,Nil> : listn(A)",
    11.1 --- a/src/ZF/ex/Prop.ML	Fri Jul 01 11:03:42 1994 +0200
    11.2 +++ b/src/ZF/ex/Prop.ML	Fri Jul 01 11:04:12 1994 +0200
    11.3 @@ -12,13 +12,10 @@
    11.4   (val thy = Univ.thy;
    11.5    val rec_specs = 
    11.6        [("prop", "univ(0)",
    11.7 -	  [(["Fls"],	"i"),
    11.8 -	   (["Var"],	"i=>i"),
    11.9 -	   (["op =>"],	"[i,i]=>i")])];
   11.10 +	  [(["Fls"],	"i",NoSyn),
   11.11 +	   (["Var"],	"i=>i", Mixfix ("#_", [100], 100)),
   11.12 +	   (["=>"],	"[i,i]=>i", Infixr 90)])];
   11.13    val rec_styp = "i";
   11.14 -  val ext = Some (Syntax.simple_sext
   11.15 -		    [OldMixfix.Mixfix("#_", "i => i", "Var", [100], 100),
   11.16 -		     OldMixfix.Infixr("=>", "[i,i] => i", 90)]);
   11.17    val sintrs = 
   11.18  	  ["Fls : prop",
   11.19  	   "n: nat ==> #n : prop",
    12.1 --- a/src/ZF/ex/Rmap.ML	Fri Jul 01 11:03:42 1994 +0200
    12.2 +++ b/src/ZF/ex/Rmap.ML	Fri Jul 01 11:04:12 1994 +0200
    12.3 @@ -7,7 +7,7 @@
    12.4  *)
    12.5  
    12.6  structure Rmap = Inductive_Fun
    12.7 - (val thy = List.thy addconsts [(["rmap"],"i=>i")];
    12.8 + (val thy = List.thy |> add_consts [("rmap","i=>i",NoSyn)];
    12.9    val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
   12.10    val sintrs = 
   12.11        ["<Nil,Nil> : rmap(r)",
    13.1 --- a/src/ZF/ex/TF.ML	Fri Jul 01 11:03:42 1994 +0200
    13.2 +++ b/src/ZF/ex/TF.ML	Fri Jul 01 11:04:12 1994 +0200
    13.3 @@ -9,12 +9,11 @@
    13.4  structure TF = Datatype_Fun
    13.5   (val thy        = Univ.thy
    13.6    val rec_specs  = [("tree", "univ(A)",
    13.7 -                       [(["Tcons"],  "[i,i]=>i")]),
    13.8 +                       [(["Tcons"],  "[i,i]=>i",NoSyn)]),
    13.9                      ("forest", "univ(A)",
   13.10 -                       [(["Fnil"],   "i"),
   13.11 -                        (["Fcons"],  "[i,i]=>i")])]
   13.12 +                       [(["Fnil"],   "i",NoSyn),
   13.13 +                        (["Fcons"],  "[i,i]=>i",NoSyn)])]
   13.14    val rec_styp   = "i=>i"
   13.15 -  val ext        = None
   13.16    val sintrs     = 
   13.17            ["[| a:A;  f: forest(A) |] ==> Tcons(a,f) : tree(A)",
   13.18             "Fnil : forest(A)",
    14.1 --- a/src/ZF/ex/Term.ML	Fri Jul 01 11:03:42 1994 +0200
    14.2 +++ b/src/ZF/ex/Term.ML	Fri Jul 01 11:04:12 1994 +0200
    14.3 @@ -11,9 +11,8 @@
    14.4   (val thy = List.thy;
    14.5    val rec_specs = 
    14.6        [("term", "univ(A)",
    14.7 -	  [(["Apply"], "[i,i]=>i")])];
    14.8 +	  [(["Apply"], "[i,i]=>i", NoSyn)])];
    14.9    val rec_styp = "i=>i";
   14.10 -  val ext = None
   14.11    val sintrs = ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
   14.12    val monos = [list_mono];
   14.13    val type_intrs = datatype_intrs;