tuned whitespace
authorhaftmann
Fri Dec 04 18:52:55 2009 +0100 (2009-12-04)
changeset 33995ebf231de0c5c
parent 33994 fc8af744f63c
child 33996 e4fb0daadcff
tuned whitespace
src/HOL/Sum_Type.thy
     1.1 --- a/src/HOL/Sum_Type.thy	Fri Dec 04 18:51:15 2009 +0100
     1.2 +++ b/src/HOL/Sum_Type.thy	Fri Dec 04 18:52:55 2009 +0100
     1.3 @@ -49,10 +49,10 @@
     1.4    by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq)
     1.5  
     1.6  definition Inl :: "'a \<Rightarrow> 'a + 'b" where
     1.7 -   "Inl = Abs_Sum \<circ> Inl_Rep"
     1.8 +  "Inl = Abs_Sum \<circ> Inl_Rep"
     1.9  
    1.10  definition Inr :: "'b \<Rightarrow> 'a + 'b" where
    1.11 -   "Inr = Abs_Sum \<circ> Inr_Rep"
    1.12 +  "Inr = Abs_Sum \<circ> Inr_Rep"
    1.13  
    1.14  lemma inj_Inl [simp]: "inj_on Inl A"
    1.15  by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI)
    1.16 @@ -160,6 +160,7 @@
    1.17    then show "f x = g x" by simp
    1.18  qed
    1.19  
    1.20 +
    1.21  subsection {* The Disjoint Sum of Sets *}
    1.22  
    1.23  definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where