src/HOL/Limits.thy
changeset 53381 355a4cac5440
parent 52265 bb907eba5902
child 53602 0ae3db699a3e
     1.1 --- a/src/HOL/Limits.thy	Tue Sep 03 19:58:00 2013 +0200
     1.2 +++ b/src/HOL/Limits.thy	Tue Sep 03 22:04:23 2013 +0200
     1.3 @@ -33,16 +33,17 @@
     1.4    "(at_infinity \<Colon> real filter) = sup at_top at_bot"
     1.5    unfolding sup_filter_def at_infinity_def eventually_at_top_linorder eventually_at_bot_linorder
     1.6  proof (intro arg_cong[where f=Abs_filter] ext iffI)
     1.7 -  fix P :: "real \<Rightarrow> bool" assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
     1.8 -  then guess r ..
     1.9 +  fix P :: "real \<Rightarrow> bool"
    1.10 +  assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
    1.11 +  then obtain r where "\<forall>x. r \<le> norm x \<longrightarrow> P x" ..
    1.12    then have "(\<forall>x\<ge>r. P x) \<and> (\<forall>x\<le>-r. P x)" by auto
    1.13    then show "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)" by auto
    1.14  next
    1.15 -  fix P :: "real \<Rightarrow> bool" assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
    1.16 +  fix P :: "real \<Rightarrow> bool"
    1.17 +  assume "(\<exists>r. \<forall>x\<ge>r. P x) \<and> (\<exists>r. \<forall>x\<le>r. P x)"
    1.18    then obtain p q where "\<forall>x\<ge>p. P x" "\<forall>x\<le>q. P x" by auto
    1.19    then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x"
    1.20 -    by (intro exI[of _ "max p (-q)"])
    1.21 -       (auto simp: abs_real_def)
    1.22 +    by (intro exI[of _ "max p (-q)"]) (auto simp: abs_real_def)
    1.23  qed
    1.24  
    1.25  lemma at_top_le_at_infinity: