--- a/src/HOL/Sum_Type.thy Fri Dec 04 18:51:15 2009 +0100
+++ b/src/HOL/Sum_Type.thy Fri Dec 04 18:52:55 2009 +0100
@@ -49,10 +49,10 @@
by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq)
definition Inl :: "'a \<Rightarrow> 'a + 'b" where
- "Inl = Abs_Sum \<circ> Inl_Rep"
+ "Inl = Abs_Sum \<circ> Inl_Rep"
definition Inr :: "'b \<Rightarrow> 'a + 'b" where
- "Inr = Abs_Sum \<circ> Inr_Rep"
+ "Inr = Abs_Sum \<circ> Inr_Rep"
lemma inj_Inl [simp]: "inj_on Inl A"
by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI)
@@ -160,6 +160,7 @@
then show "f x = g x" by simp
qed
+
subsection {* The Disjoint Sum of Sets *}
definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where