# 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 ***)