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:
```