fixed tex problem
authornipkow
Wed Aug 04 09:44:40 2004 +0200 (2004-08-04)
changeset 15105e194d4d265fb
parent 15104 f14e0d9587be
child 15106 e8cef6993701
fixed tex problem
src/HOL/Hyperreal/Integration.thy
     1.1 --- a/src/HOL/Hyperreal/Integration.thy	Tue Aug 03 14:48:59 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/Integration.thy	Wed Aug 04 09:44:40 2004 +0200
     1.3 @@ -369,7 +369,7 @@
     1.4  
     1.5  text{*Fundamental theorem of calculus (Part I)*}
     1.6  
     1.7 -text{*"Straddle Lemma" : Swartz & Thompson: AMM 95(7) 1988 *}
     1.8 +text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}
     1.9  
    1.10  lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))"
    1.11  by meson