src/HOL/Sum_Type.thy
changeset 31080 21ffc770ebc0
parent 29183 f1648e009dc1
child 33961 03f2ab6a4ea6
     1.1 --- a/src/HOL/Sum_Type.thy	Fri May 08 19:20:00 2009 +0200
     1.2 +++ b/src/HOL/Sum_Type.thy	Sat May 09 07:25:22 2009 +0200
     1.3 @@ -157,6 +157,8 @@
     1.4  apply auto
     1.5  done
     1.6  
     1.7 +lemma Plus_eq_empty_conv[simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
     1.8 +by(auto)
     1.9  
    1.10  subsection{*The @{term Part} Primitive*}
    1.11