src/HOL/Datatype.thy
changeset 29025 8c8859c0d734
parent 28689 2947dc320178
child 29183 f1648e009dc1
     1.1 --- a/src/HOL/Datatype.thy	Tue Dec 09 12:53:25 2008 -0800
     1.2 +++ b/src/HOL/Datatype.thy	Tue Dec 09 15:31:38 2008 -0800
     1.3 @@ -605,6 +605,9 @@
     1.4  lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
     1.5    by (rule set_ext, case_tac x) auto
     1.6  
     1.7 +lemma inj_Some [simp]: "inj_on Some A"
     1.8 +  by (rule inj_onI) simp
     1.9 +
    1.10  
    1.11  subsubsection {* Operations *}
    1.12