src/HOL/Real/HahnBanach/Bounds.thy
changeset 27612 d3eb431db035
parent 27611 2c01c0bdb385
child 29043 409d1ca929b5
     1.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Tue Jul 15 16:50:09 2008 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Tue Jul 15 19:39:37 2008 +0200
     1.3 @@ -28,7 +28,8 @@
     1.4    shows "\<Squnion>A = (x::'a::order)"
     1.5  proof -
     1.6    interpret lub [A x] by fact
     1.7 -  show ?thesis proof (unfold the_lub_def)
     1.8 +  show ?thesis
     1.9 +  proof (unfold the_lub_def)
    1.10      from `lub A x` show "The (lub A) = x"
    1.11      proof
    1.12        fix x' assume lub': "lub A x'"
    1.13 @@ -73,7 +74,7 @@
    1.14    shows "\<exists>x. lub A x"
    1.15  proof -
    1.16    from ex_upper have "\<exists>y. isUb UNIV A y"
    1.17 -    by (unfold isUb_def setle_def) blast
    1.18 +    unfolding isUb_def setle_def by blast
    1.19    with nonempty have "\<exists>x. isLub UNIV A x"
    1.20      by (rule reals_complete)
    1.21    then show ?thesis by (simp only: lub_compat)