Inductive defs need no longer mention SigmaI/E2

--- 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 = [e-mail]@[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 = [e-mail]@[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);