--- a/src/ZF/ex/Acc.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Acc.ML Fri Jul 01 11:04:12 1994 +0200
@@ -10,7 +10,7 @@
*)
structure Acc = Inductive_Fun
- (val thy = WF.thy addconsts [(["acc"],"i=>i")]
+ (val thy = WF.thy |> add_consts [("acc","i=>i",NoSyn)]
val rec_doms = [("acc", "field(r)")]
val sintrs = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
val monos = [Pow_mono]
--- a/src/ZF/ex/BT.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/BT.ML Fri Jul 01 11:04:12 1994 +0200
@@ -10,9 +10,9 @@
(val thy = Univ.thy;
val rec_specs =
[("bt", "univ(A)",
- [(["Lf"],"i"), (["Br"],"[i,i,i]=>i")])];
+ [(["Lf"],"i",NoSyn),
+ (["Br"],"[i,i,i]=>i", NoSyn)])];
val rec_styp = "i=>i";
- val ext = None
val sintrs =
["Lf : bt(A)",
"[| a: A; t1: bt(A); t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
--- a/src/ZF/ex/Bin.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Bin.ML Fri Jul 01 11:04:12 1994 +0200
@@ -11,11 +11,9 @@
(val thy = Univ.thy;
val rec_specs =
[("bin", "univ(0)",
- [(["Plus", "Minus"], "i"),
- (["op $$"], "[i,i]=>i")])];
+ [(["Plus", "Minus"], "i", NoSyn),
+ (["$$"], "[i,i]=>i", Infixl 60)])];
val rec_styp = "i";
- val ext = Some (Syntax.simple_sext
- [OldMixfix.Infixl("$$", "[i,i] => i", 60)]);
val sintrs =
["Plus : bin",
"Minus : bin",
--- a/src/ZF/ex/CoUnit.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/CoUnit.ML Fri Jul 01 11:04:12 1994 +0200
@@ -16,9 +16,8 @@
(val thy = QUniv.thy;
val rec_specs =
[("counit", "quniv(0)",
- [(["Con"], "i=>i")])];
+ [(["Con"], "i=>i", NoSyn)])];
val rec_styp = "i";
- val ext = None
val sintrs = ["x: counit ==> Con(x) : counit"];
val monos = [];
val type_intrs = codatatype_intrs
@@ -53,9 +52,8 @@
(val thy = QUniv.thy;
val rec_specs =
[("counit2", "quniv(0)",
- [(["Con2"], "[i,i]=>i")])];
+ [(["Con2"], "[i,i]=>i", NoSyn)])];
val rec_styp = "i";
- val ext = None
val sintrs = ["[| x: counit2; y: counit2 |] ==> Con2(x,y) : counit2"];
val monos = [];
val type_intrs = codatatype_intrs
--- a/src/ZF/ex/Comb.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Comb.ML Fri Jul 01 11:04:12 1994 +0200
@@ -16,11 +16,9 @@
(val thy = Univ.thy;
val rec_specs =
[("comb", "univ(0)",
- [(["K","S"], "i"),
- (["op #"], "[i,i]=>i")])];
+ [(["K","S"], "i", NoSyn),
+ (["#"], "[i,i]=>i", Infixl 90)])];
val rec_styp = "i";
- val ext = Some (Syntax.simple_sext
- [OldMixfix.Infixl("#", "[i,i] => i", 90)]);
val sintrs =
["K : comb",
"S : comb",
--- a/src/ZF/ex/Data.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Data.ML Fri Jul 01 11:04:12 1994 +0200
@@ -10,12 +10,11 @@
structure Data = Datatype_Fun
(val thy = Univ.thy
val rec_specs = [("data", "univ(A Un B)",
- [(["Con0"], "i"),
- (["Con1"], "i=>i"),
- (["Con2"], "[i,i]=>i"),
- (["Con3"], "[i,i,i]=>i")])]
+ [(["Con0"], "i",NoSyn),
+ (["Con1"], "i=>i",NoSyn),
+ (["Con2"], "[i,i]=>i",NoSyn),
+ (["Con3"], "[i,i,i]=>i",NoSyn)])]
val rec_styp = "[i,i]=>i"
- val ext = None
val sintrs =
["Con0 : data(A,B)",
"[| a: A |] ==> Con1(a) : data(A,B)",
--- a/src/ZF/ex/Enum.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Enum.ML Fri Jul 01 11:04:12 1994 +0200
@@ -19,9 +19,8 @@
(val thy = Univ.thy;
val rec_specs =
[("enum", "univ(0)",
- [(consts, "i")])];
+ [(consts, "i", NoSyn)])];
val rec_styp = "i";
- val ext = None
val sintrs = map (fn const => const ^ " : enum") consts;
val monos = [];
val type_intrs = datatype_intrs
--- a/src/ZF/ex/LList.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/LList.ML Fri Jul 01 11:04:12 1994 +0200
@@ -9,10 +9,9 @@
structure LList = CoDatatype_Fun
(val thy = QUniv.thy
val rec_specs = [("llist", "quniv(A)",
- [(["LNil"], "i"),
- (["LCons"], "[i,i]=>i")])]
+ [(["LNil"], "i",NoSyn),
+ (["LCons"], "[i,i]=>i",NoSyn)])]
val rec_styp = "i=>i"
- val ext = None
val sintrs = ["LNil : llist(A)",
"[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"]
val monos = []
--- a/src/ZF/ex/LList_Eq.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/LList_Eq.ML Fri Jul 01 11:04:12 1994 +0200
@@ -11,7 +11,7 @@
a q/Q to the Sigma, Pair and converse rules.*)
structure LList_Eq = CoInductive_Fun
- (val thy = LList.thy addconsts [(["lleq"],"i=>i")]
+ (val thy = LList.thy |> add_consts [("lleq","i=>i",NoSyn)]
val rec_doms = [("lleq", "llist(A) * llist(A)")]
val sintrs =
["<LNil, LNil> : lleq(A)",
--- a/src/ZF/ex/ListN.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/ListN.ML Fri Jul 01 11:04:12 1994 +0200
@@ -10,7 +10,7 @@
*)
structure ListN = Inductive_Fun
- (val thy = ListFn.thy addconsts [(["listn"],"i=>i")]
+ (val thy = ListFn.thy |> add_consts [("listn","i=>i",NoSyn)]
val rec_doms = [("listn", "nat*list(A)")]
val sintrs =
["<0,Nil> : listn(A)",
--- a/src/ZF/ex/Prop.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Prop.ML Fri Jul 01 11:04:12 1994 +0200
@@ -12,13 +12,10 @@
(val thy = Univ.thy;
val rec_specs =
[("prop", "univ(0)",
- [(["Fls"], "i"),
- (["Var"], "i=>i"),
- (["op =>"], "[i,i]=>i")])];
+ [(["Fls"], "i",NoSyn),
+ (["Var"], "i=>i", Mixfix ("#_", [100], 100)),
+ (["=>"], "[i,i]=>i", Infixr 90)])];
val rec_styp = "i";
- val ext = Some (Syntax.simple_sext
- [OldMixfix.Mixfix("#_", "i => i", "Var", [100], 100),
- OldMixfix.Infixr("=>", "[i,i] => i", 90)]);
val sintrs =
["Fls : prop",
"n: nat ==> #n : prop",
--- a/src/ZF/ex/Rmap.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Rmap.ML Fri Jul 01 11:04:12 1994 +0200
@@ -7,7 +7,7 @@
*)
structure Rmap = Inductive_Fun
- (val thy = List.thy addconsts [(["rmap"],"i=>i")];
+ (val thy = List.thy |> add_consts [("rmap","i=>i",NoSyn)];
val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
val sintrs =
["<Nil,Nil> : rmap(r)",
--- a/src/ZF/ex/TF.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/TF.ML Fri Jul 01 11:04:12 1994 +0200
@@ -9,12 +9,11 @@
structure TF = Datatype_Fun
(val thy = Univ.thy
val rec_specs = [("tree", "univ(A)",
- [(["Tcons"], "[i,i]=>i")]),
+ [(["Tcons"], "[i,i]=>i",NoSyn)]),
("forest", "univ(A)",
- [(["Fnil"], "i"),
- (["Fcons"], "[i,i]=>i")])]
+ [(["Fnil"], "i",NoSyn),
+ (["Fcons"], "[i,i]=>i",NoSyn)])]
val rec_styp = "i=>i"
- val ext = None
val sintrs =
["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)",
"Fnil : forest(A)",
--- a/src/ZF/ex/Term.ML Fri Jul 01 11:03:42 1994 +0200
+++ b/src/ZF/ex/Term.ML Fri Jul 01 11:04:12 1994 +0200
@@ -11,9 +11,8 @@
(val thy = List.thy;
val rec_specs =
[("term", "univ(A)",
- [(["Apply"], "[i,i]=>i")])];
+ [(["Apply"], "[i,i]=>i", NoSyn)])];
val rec_styp = "i=>i";
- val ext = None
val sintrs = ["[| a: A; l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
val monos = [list_mono];
val type_intrs = datatype_intrs;