src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy

 (*  Title:      HOL/HOLCF/IOA/meta_theory/Deadlock.thy
     Author:     Olaf Müller
 *)
 
-section {* Deadlock freedom of I/O Automata *}
+section \<open>Deadlock freedom of I/O Automata\<close>
 
 theory Deadlock
 imports RefCorrectness CompoScheds
 begin
 
-text {* input actions may always be added to a schedule *}
+text \<open>input actions may always be added to a schedule\<close>
 
 lemma scheds_input_enabled:
   "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|]  
           ==> Filter (%x. x:act A)$sch @@ a\<leadsto>nil : schedules A"
 apply (simp add: schedules_def has_schedule_def)
 apply auto
 apply (frule inp_is_act)
 apply (simp add: executions_def)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
 apply (rename_tac s ex)
 apply (subgoal_tac "Finite ex")
 prefer 2
 apply (simp add: filter_act_def)
 defer

 apply simp
 apply (rule sym)
 apply assumption
 done
 
-text {*
+text \<open>
                Deadlock freedom: component B cannot block an out or int action
                                  of component A in every schedule.
     Needs compositionality on schedule level, input-enabledness, compatibility
                     and distributivity of is_exec_frag over @@
-*}
+\<close>
 
 declare split_if [split del]
 lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A\<parallel>B);  
              Filter (%x. x:act A)$(sch @@ a\<leadsto>nil) : schedules A; compatible A B; input_enabled B |]  
            ==> (sch @@ a\<leadsto>nil) : schedules (A\<parallel>B)"