diff -r f32931b93686 -r 2fcc6017cb72 src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Mon Feb 07 15:28:43 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Mon Feb 07 18:38:51 2000 +0100
@@ -10,8 +10,8 @@
 text {* Some existing theorems are declared as extra introduction
 or elimination rules, respectively. *};
 
-lemmas [intro!!] = isLub_isUb;
-lemmas [intro!!] = chainD; 
+lemmas [intro??] = isLub_isUb;
+lemmas [intro??] = chainD; 
 lemmas chainE2 = chainD2 [elimify];
 
 text_raw {* \medskip *};