diff -r f075640b8868 -r 3abf6a722518 src/HOL/Hoare_Parallel/OG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/OG_Hoare.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -120,19 +120,19 @@
 apply (unfold com_validity_def)
 apply(rule oghoare_induct)
 apply simp_all
-\<comment>\<open>Basic\<close>
+\<comment> \<open>Basic\<close>
     apply(simp add: SEM_def sem_def)
     apply(fast dest: rtrancl_imp_UN_relpow Basic_ntran)
-\<comment>\<open>Seq\<close>
+\<comment> \<open>Seq\<close>
    apply(rule impI)
    apply(rule subset_trans)
     prefer 2 apply simp
    apply(simp add: L3_5ii L3_5i)
-\<comment>\<open>Cond\<close>
+\<comment> \<open>Cond\<close>
   apply(simp add: L3_5iv)
-\<comment>\<open>While\<close>
+\<comment> \<open>While\<close>
  apply (force simp add: L3_5v dest: SEM_fwhile)
-\<comment>\<open>Conseq\<close>
+\<comment> \<open>Conseq\<close>
 apply(force simp add: SEM_def sem_def)
 done
 
@@ -175,11 +175,11 @@
  (\<forall>q. \<turnstile> c q \<longrightarrow> (if co' = None then t\<in>q else t \<in> pre(the co') \<and> \<turnstile> (the co') q )))"
 apply(rule ann_transition_transition.induct [THEN conjunct1])
 apply simp_all
-\<comment>\<open>Basic\<close>
+\<comment> \<open>Basic\<close>
          apply clarify
          apply(frule ann_hoare_case_analysis)
          apply force
-\<comment>\<open>Seq\<close>
+\<comment> \<open>Seq\<close>
         apply clarify
         apply(frule ann_hoare_case_analysis,simp)
         apply(fast intro: AnnConseq)
@@ -190,21 +190,21 @@
         apply force
        apply(rule AnnSeq,simp)
        apply(fast intro: AnnConseq)
-\<comment>\<open>Cond1\<close>
+\<comment> \<open>Cond1\<close>
       apply clarify
       apply(frule ann_hoare_case_analysis,simp)
       apply(fast intro: AnnConseq)
      apply clarify
      apply(frule ann_hoare_case_analysis,simp)
      apply(fast intro: AnnConseq)
-\<comment>\<open>Cond2\<close>
+\<comment> \<open>Cond2\<close>
     apply clarify
     apply(frule ann_hoare_case_analysis,simp)
     apply(fast intro: AnnConseq)
    apply clarify
    apply(frule ann_hoare_case_analysis,simp)
    apply(fast intro: AnnConseq)
-\<comment>\<open>While\<close>
+\<comment> \<open>While\<close>
   apply clarify
   apply(frule ann_hoare_case_analysis,simp)
   apply force
@@ -215,7 +215,7 @@
   apply simp
  apply(rule AnnWhile)
   apply simp_all
-\<comment>\<open>Await\<close>
+\<comment> \<open>Await\<close>
 apply(frule ann_hoare_case_analysis,simp)
 apply clarify
 apply(drule atom_hoare_sound)
@@ -349,7 +349,7 @@
 prefer 11
 apply(rule TrueI)
 apply simp_all
-\<comment>\<open>Basic\<close>
+\<comment> \<open>Basic\<close>
    apply(erule_tac x = "i" in all_dupE, erule (1) notE impE)
    apply(erule_tac x = "j" in allE , erule (1) notE impE)
    apply(simp add: interfree_def)
@@ -366,12 +366,12 @@
     apply(force intro: converse_rtrancl_into_rtrancl
           simp add: com_validity_def SEM_def sem_def All_None_def)
    apply(simp add:assertions_lemma)
-\<comment>\<open>Seqs\<close>
+\<comment> \<open>Seqs\<close>
   apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
   apply(drule  Parallel_Strong_Soundness_Seq,simp+)
  apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
  apply(drule  Parallel_Strong_Soundness_Seq,simp+)
-\<comment>\<open>Await\<close>
+\<comment> \<open>Await\<close>
 apply(rule_tac x = "i" in allE , assumption , erule (1) notE impE)
 apply(erule_tac x = "j" in allE , erule (1) notE impE)
 apply(simp add: interfree_def)
@@ -398,9 +398,9 @@
   else t\<in>pre(the(com(Rs ! j))) \<and> \<turnstile> the(com(Rs ! j)) post(Ts ! j))) \<and> interfree Rs"
 apply(erule rtrancl_induct2)
  apply clarify
-\<comment>\<open>Base\<close>
+\<comment> \<open>Base\<close>
  apply force
-\<comment>\<open>Induction step\<close>
+\<comment> \<open>Induction step\<close>
 apply clarify
 apply(drule Parallel_length_post_PStar)
 apply clarify
@@ -432,7 +432,7 @@
 apply (unfold com_validity_def)
 apply(rule oghoare_induct)
 apply(rule TrueI)+
-\<comment>\<open>Parallel\<close>
+\<comment> \<open>Parallel\<close>
       apply(simp add: SEM_def sem_def)
       apply(clarify, rename_tac x y i Ts')
       apply(frule Parallel_length_post_PStar)
@@ -446,19 +446,19 @@
       apply(drule_tac s = "length Rs" in sym)
       apply(erule allE, erule impE, assumption)
       apply(force dest: nth_mem simp add: All_None_def)
-\<comment>\<open>Basic\<close>
+\<comment> \<open>Basic\<close>
     apply(simp add: SEM_def sem_def)
     apply(force dest: rtrancl_imp_UN_relpow Basic_ntran)
-\<comment>\<open>Seq\<close>
+\<comment> \<open>Seq\<close>
    apply(rule subset_trans)
     prefer 2 apply assumption
    apply(simp add: L3_5ii L3_5i)
-\<comment>\<open>Cond\<close>
+\<comment> \<open>Cond\<close>
   apply(simp add: L3_5iv)
-\<comment>\<open>While\<close>
+\<comment> \<open>While\<close>
  apply(simp add: L3_5v)
  apply (blast dest: SEM_fwhile)
-\<comment>\<open>Conseq\<close>
+\<comment> \<open>Conseq\<close>
 apply(auto simp add: SEM_def sem_def)
 done