# HG changeset patch
# User lcp
# Date 782729885 -3600
# Node ID ff4d4d7fcb7f6e63fbd40f421e46236f650041d4
# Parent  4b0455fbcc49c9736e966672a80d3379f9a3ff3e
ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
definitions may involve ordinary pairs.  (HOL/intr_elim does not require
this change)

diff -r 4b0455fbcc49 -r ff4d4d7fcb7f src/ZF/intr_elim.ML
--- a/src/ZF/intr_elim.ML	Fri Oct 21 09:53:38 1994 +0100
+++ b/src/ZF/intr_elim.ML	Fri Oct 21 09:58:05 1994 +0100
@@ -119,9 +119,12 @@
 
 (*Includes rules for succ and Pair since they are common constructions*)
 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
-		Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject, 
+		Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
+		make_elim succ_inject, 
 		refl_thin, conjE, exE, disjE];
 
+(*Standard sum/products for datatypes, variant ones for codatatypes;
+  We always include Pair_inject above*)
 val sumprod_free_SEs = 
     map (gen_make_elim [conjE,FalseE])
 	([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]