changeset 8280 | 259073d16f84 |
parent 8203 | 2fcc6017cb72 |
child 8703 | 816d8f6513be |
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Feb 22 21:48:50 2000 +0100 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Tue Feb 22 21:49:34 2000 +0100 @@ -253,7 +253,7 @@ txt{* The proof is by case analysis on $x$. *}; show ?thesis; - proof (rule case_split); + proof cases; txt {* For the case $x = \zero$ the thesis follows from the linearity of $f$: for every linear function