# HG changeset patch
# User paulson
# Date 820148055 -3600
# Node ID 5726a8243d3f009b83f1c498f6d1f657e6f5f03c
# Parent  bc628f4ef0cb4644f1c6a4a68dea3a85a506f60b
fixed indentation

diff -r bc628f4ef0cb -r 5726a8243d3f src/HOL/Sum.thy
--- a/src/HOL/Sum.thy	Sat Dec 23 12:50:53 1995 +0100
+++ b/src/HOL/Sum.thy	Thu Dec 28 11:54:15 1995 +0100
@@ -41,7 +41,7 @@
   Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
   Inr_def       "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
   sum_case_def  "sum_case f g p == @z.  (!x. p=Inl(x) --> z=f(x))      
-                                     & (!y. p=Inr(y) --> z=g(y))"
+                                      & (!y. p=Inr(y) --> z=g(y))"
 
   sum_def       "A plus B == (Inl``A) Un (Inr``B)"