diff -r f075640b8868 -r 3abf6a722518 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/NanoJava/AxSem.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -72,13 +72,13 @@
                   Impl (D,m) {Q} ==>
              A \<turnstile> {P} Meth (C,m) {Q}"
 
-  \<comment>\<open>\<open>\<Union>Z\<close> instead of \<open>\<forall>Z\<close> in the conclusion and\\
+  \<comment> \<open>\<open>\<Union>Z\<close> instead of \<open>\<forall>Z\<close> in the conclusion and\\
        Z restricted to type state due to limitations of the inductive package\<close>
 | Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
                             (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
                       A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
 
-\<comment>\<open>structural rules\<close>
+\<comment> \<open>structural rules\<close>
 
 | Asm:  "   a \<in> A ==> A |\<turnstile> {a}"
 
@@ -86,12 +86,12 @@
 
 | ConjE: "[|A |\<turnstile> C; c \<in> C |] ==> A |\<turnstile> {c}"
 
-  \<comment>\<open>Z restricted to type state due to limitations of the inductive package\<close>
+  \<comment> \<open>Z restricted to type state due to limitations of the inductive package\<close>
 | Conseq:"[| \<forall>Z::state. A \<turnstile> {P' Z} c {Q' Z};
              \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
             A \<turnstile> {P} c {Q }"
 
-  \<comment>\<open>Z restricted to type state due to limitations of the inductive package\<close>
+  \<comment> \<open>Z restricted to type state due to limitations of the inductive package\<close>
 | eConseq:"[| \<forall>Z::state. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
              \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
             A \<turnstile>\<^sub>e {P} e {Q }"