src/HOL/Library/Continuity.thy
changeset 32456 341c83339aeb
parent 30971 7fbebf75b3ef
child 32960 69916a850301
     1.1 --- a/src/HOL/Library/Continuity.thy	Sat Aug 29 14:31:39 2009 +0200
     1.2 +++ b/src/HOL/Library/Continuity.thy	Mon Aug 31 14:09:42 2009 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4   apply (rule up_chainI)
     1.5   apply simp
     1.6  apply (drule Un_absorb1)
     1.7 -apply (auto simp add: nat_not_singleton)
     1.8 +apply (auto split:split_if_asm)
     1.9  done
    1.10  
    1.11  
    1.12 @@ -184,8 +184,7 @@
    1.13   apply (rule down_chainI)
    1.14   apply simp
    1.15  apply (drule Int_absorb1)
    1.16 -apply auto
    1.17 -apply (auto simp add: nat_not_singleton)
    1.18 +apply (auto split:split_if_asm)
    1.19  done
    1.20  
    1.21