src/HOL/Library/Continuity.thy
changeset 11461 ffeac9aa1967
parent 11355 778c369559d9
child 14706 71590b7733b7
     1.1 --- a/src/HOL/Library/Continuity.thy	Mon Aug 06 12:41:21 2001 +0200
     1.2 +++ b/src/HOL/Library/Continuity.thy	Mon Aug 06 12:42:43 2001 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4     apply (rule up_chainI)
     1.5     apply  simp+
     1.6    apply (drule Un_absorb1)
     1.7 -  apply auto
     1.8 +  apply (auto simp add: nat_not_singleton)
     1.9    done
    1.10  
    1.11  
    1.12 @@ -110,7 +110,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    done
    1.19  
    1.20