| changeset 32456 | 341c83339aeb |
| parent 30971 | 7fbebf75b3ef |
| child 32960 | 69916a850301 |
--- a/src/HOL/Library/Continuity.thy Sat Aug 29 14:31:39 2009 +0200 +++ b/src/HOL/Library/Continuity.thy Mon Aug 31 14:09:42 2009 +0200 @@ -156,7 +156,7 @@ apply (rule up_chainI) apply simp apply (drule Un_absorb1) -apply (auto simp add: nat_not_singleton) +apply (auto split:split_if_asm) done @@ -184,8 +184,7 @@ apply (rule down_chainI) apply simp apply (drule Int_absorb1) -apply auto -apply (auto simp add: nat_not_singleton) +apply (auto split:split_if_asm) done