# HG changeset patch
# User haftmann
# Date 1259949175 -3600
# Node ID ebf231de0c5cecf0ef60cf9c47ae9038355c6ec9
# Parent  fc8af744f63c47b93b3e6ec9294fac8a94036715
tuned whitespace

diff -r fc8af744f63c -r ebf231de0c5c src/HOL/Sum_Type.thy
--- 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