src/HOL/Datatype.thy

--- a/src/HOL/Datatype.thy	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Datatype.thy	Tue Nov 12 13:47:24 2013 +0100
@@ -499,7 +499,7 @@
 
 (*Dependent version*)
 lemma dprod_subset_Sigma2:
-     "(dprod (Sigma A B) (Sigma C D)) <= 
+     "(dprod (Sigma A B) (Sigma C D)) <=
       Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"
 by auto
 
@@ -522,4 +522,3 @@
 setup Datatype_Realizer.setup
 
 end
-