# HG changeset patch
# User paulson
# Date 865585270 -7200
# Node ID be777156c7e98052c86765dfdadd03490009fb96
# Parent  02dc9c5b035fc6976194dc6021ed9c73fa4cc07e
New facts about In0/1 by Burkhart Wolff

diff -r 02dc9c5b035f -r be777156c7e9 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Fri Jun 06 10:20:38 1997 +0200
+++ b/src/HOL/Univ.ML	Fri Jun 06 10:21:10 1997 +0200
@@ -354,7 +354,24 @@
 by (rtac (major RS Scons_inject2) 1);
 qed "In1_inject";
 
-AddSDs [In0_inject, In1_inject];
+goal Univ.thy "(In0 M = In0 N) = (M=N)";
+by (blast_tac (!claset addSDs [In0_inject]) 1);
+qed "In0_eq";
+
+goal Univ.thy "(In1 M = In1 N) = (M=N)";
+by (blast_tac (!claset addSDs [In1_inject]) 1);
+qed "In1_eq";
+
+AddIffs [In0_eq, In1_eq];
+
+goalw Univ.thy [inj_def] "inj In0";
+by (Blast_tac 1);
+qed "inj_In0";
+
+goalw Univ.thy [inj_def] "inj In1";
+by (Blast_tac 1);
+qed "inj_In1";
+
 
 (*** proving equality of sets and functions using ntrunc ***)