--- a/src/ZF/IMP/Evala.ML Fri Jul 29 11:03:23 1994 +0200
+++ b/src/ZF/IMP/Evala.ML Fri Jul 29 11:09:45 1994 +0200
@@ -21,6 +21,6 @@
val monos = [];
val con_defs = [];
- val type_intrs = Aexp.intrs@[SigmaI,apply_funtype];
- val type_elims = [SigmaE2]
+ val type_intrs = Aexp.intrs@[apply_funtype];
+ val type_elims = []
);
--- a/src/ZF/IMP/Evalb.ML Fri Jul 29 11:03:23 1994 +0200
+++ b/src/ZF/IMP/Evalb.ML Fri Jul 29 11:09:45 1994 +0200
@@ -25,7 +25,7 @@
val monos = [];
val con_defs = [];
- val type_intrs = Bexp.intrs@[SigmaI,apply_funtype,and_type,or_type,
+ val type_intrs = Bexp.intrs@[apply_funtype,and_type,or_type,
bool_1I,bool_0I,not_type];
- val type_elims = [SigmaE2,make_elim(Evala.dom_subset RS subsetD) ];
+ val type_elims = [make_elim(Evala.dom_subset RS subsetD) ];
);
--- a/src/ZF/IMP/Evalc.ML Fri Jul 29 11:03:23 1994 +0200
+++ b/src/ZF/IMP/Evalc.ML Fri Jul 29 11:09:45 1994 +0200
@@ -28,6 +28,6 @@
val monos = [];
val con_defs = [assign_def];
- val type_intrs = Bexp.intrs@Com.intrs@[SigmaI,if_type,lam_type,apply_type];
- val type_elims = [SigmaE2,make_elim(Evala.dom_subset RS subsetD),
- make_elim(Evalb.dom_subset RS subsetD) ]);
+ val type_intrs = Bexp.intrs@Com.intrs@[if_type,lam_type,apply_type];
+ val type_elims = [make_elim(Evala.dom_subset RS subsetD),
+ make_elim(Evalb.dom_subset RS subsetD) ]);
--- a/src/ZF/ex/Contract0.ML Fri Jul 29 11:03:23 1994 +0200
+++ b/src/ZF/ex/Contract0.ML Fri Jul 29 11:09:45 1994 +0200
@@ -9,18 +9,18 @@
open Contract0;
structure Contract = Inductive_Fun
- (val thy = Contract0.thy;
- val thy_name = "Contract";
- val rec_doms = [("contract","comb*comb")];
- val sintrs =
+ (val thy = Contract0.thy;
+ val thy_name = "Contract";
+ val rec_doms = [("contract","comb*comb")];
+ val sintrs =
["[| p:comb; q:comb |] ==> K#p#q -1-> p",
"[| p:comb; q:comb; r:comb |] ==> S#p#q#r -1-> (p#r)#(q#r)",
"[| p-1->q; r:comb |] ==> p#r -1-> q#r",
"[| p-1->q; r:comb |] ==> r#p -1-> r#q"];
- val monos = [];
- val con_defs = [];
- val type_intrs = Comb.intrs@[SigmaI];
- val type_elims = [SigmaE2]);
+ val monos = [];
+ val con_defs = [];
+ val type_intrs = Comb.intrs;
+ val type_elims = []);
val [K_contract,S_contract,Ap_contract1,Ap_contract2] = Contract.intrs;
--- a/src/ZF/ex/LList_Eq.ML Fri Jul 29 11:03:23 1994 +0200
+++ b/src/ZF/ex/LList_Eq.ML Fri Jul 29 11:09:45 1994 +0200
@@ -11,16 +11,16 @@
a q/Q to the Sigma, Pair and converse rules.*)
structure LList_Eq = CoInductive_Fun
- (val thy = LList.thy |> add_consts [("lleq","i=>i",NoSyn)]
- val thy_name = "LList_Eq"
+ (val thy = LList.thy |> add_consts [("lleq","i=>i",NoSyn)]
+ val thy_name = "LList_Eq"
val rec_doms = [("lleq", "llist(A) * llist(A)")]
val sintrs =
["<LNil, LNil> : lleq(A)",
"[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"]
val monos = []
val con_defs = []
- val type_intrs = LList.intrs @ [SigmaI]
- val type_elims = [SigmaE2]);
+ val type_intrs = LList.intrs
+ val type_elims = []);
(** Alternatives for above:
val con_defs = LList.con_defs
--- a/src/ZF/ex/ListN.ML Fri Jul 29 11:03:23 1994 +0200
+++ b/src/ZF/ex/ListN.ML Fri Jul 29 11:09:45 1994 +0200
@@ -18,8 +18,8 @@
"[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
val monos = []
val con_defs = []
- val type_intrs = nat_typechecks @ List.intrs @ [SigmaI]
- val type_elims = [SigmaE2]);
+ val type_intrs = nat_typechecks @ List.intrs
+ val type_elims = []);
val listn_induct = standard
(ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
--- a/src/ZF/ex/ParContract.ML Fri Jul 29 11:03:23 1994 +0200
+++ b/src/ZF/ex/ParContract.ML Fri Jul 29 11:09:45 1994 +0200
@@ -10,18 +10,18 @@
*)
structure ParContract = Inductive_Fun
- (val thy = Contract.thy;
- val thy_name = "ParContract";
- val rec_doms = [("parcontract","comb*comb")];
- val sintrs =
+ (val thy = Contract.thy;
+ val thy_name = "ParContract";
+ val rec_doms = [("parcontract","comb*comb")];
+ val sintrs =
["[| p:comb |] ==> p =1=> p",
"[| p:comb; q:comb |] ==> K#p#q =1=> p",
"[| p:comb; q:comb; r:comb |] ==> S#p#q#r =1=> (p#r)#(q#r)",
"[| p=1=>q; r=1=>s |] ==> p#r =1=> q#s"];
- val monos = [];
- val con_defs = [];
- val type_intrs = Comb.intrs@[SigmaI];
- val type_elims = [SigmaE2]);
+ val monos = [];
+ val con_defs = [];
+ val type_intrs = Comb.intrs;
+ val type_elims = []);
val [parcontract_refl,K_parcontract,S_parcontract,Ap_parcontract] =
ParContract.intrs;
--- a/src/ZF/ex/Rmap.ML Fri Jul 29 11:03:23 1994 +0200
+++ b/src/ZF/ex/Rmap.ML Fri Jul 29 11:09:45 1994 +0200
@@ -7,18 +7,18 @@
*)
structure Rmap = Inductive_Fun
- (val thy = List.thy |> add_consts [("rmap","i=>i",NoSyn)];
- val thy_name = "Rmap";
- val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
- val sintrs =
+ (val thy = List.thy |> add_consts [("rmap","i=>i",NoSyn)];
+ val thy_name = "Rmap";
+ val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
+ val sintrs =
["<Nil,Nil> : rmap(r)",
"[| <x,y>: r; <xs,ys> : rmap(r) |] ==> \
\ <Cons(x,xs), Cons(y,ys)> : rmap(r)"];
- val monos = [];
- val con_defs = [];
- val type_intrs = [domainI,rangeI] @ List.intrs @ [SigmaI]
- val type_elims = [SigmaE2]);
+ val monos = [];
+ val con_defs = [];
+ val type_intrs = [domainI,rangeI] @ List.intrs
+ val type_elims = []);
goalw Rmap.thy Rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
by (rtac lfp_mono 1);