--- a/src/HOL/Library/Infinite_Set.thy Sat Mar 03 21:00:31 2012 +0100 +++ b/src/HOL/Library/Infinite_Set.thy Sat Mar 03 21:01:23 2012 +0100 @@ -589,3 +589,4 @@ by (simp add: atmost_one_def) end +