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