diff -r 6539627881e8 -r 65d98faa2182 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Mon Sep 10 17:35:22 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy	Mon Sep 10 18:18:04 2001 +0200
@@ -86,8 +86,8 @@
                   Impl (D,m) {Q} ==>
              A |- {P} Meth (C,m) {Q}"
 
-  --{*\<Union>z instead of \<forall>z in the conclusion and
-      z restricted to type state due to limitations of the inductive package *}
+  --{* @{text "\<Union>z"} instead of @{text "\<forall>z"} in the conclusion and
+       z restricted to type state due to limitations of the inductive package *}
   Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) ||- 
                             (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms ==>
                       A ||- (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms"