src/HOL/SEQ.thy
changeset 32436 10cd49e0c067
parent 32064 53ca12ff305d
child 32707 836ec9d0a0c8
     1.1 --- a/src/HOL/SEQ.thy	Fri Aug 28 18:11:42 2009 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Fri Aug 28 18:52:41 2009 +0200
     1.3 @@ -582,7 +582,7 @@
     1.4        ultimately
     1.5        have "a (max no n) < a n" by auto
     1.6        with monotone[where m=n and n="max no n"]
     1.7 -      show False by auto
     1.8 +      show False by (auto simp:max_def split:split_if_asm)
     1.9      qed
    1.10    } note top_down = this
    1.11    { fix x n m fix a :: "nat \<Rightarrow> real"