src/HOL/Real/HahnBanach/Aux.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10606 e3229a37d53f
     1.1 --- a/src/HOL/Real/HahnBanach/Aux.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  lemmas [intro?] = isLub_isUb
     1.6  lemmas [intro?] = chainD 
     1.7 -lemmas chainE2 = chainD2 [elimified]
     1.8 +lemmas chainE2 = chainD2 [elim_format, standard]
     1.9  
    1.10  text_raw {* \medskip *}
    1.11  text{* Lemmas about sets. *}