src/HOL/HOLCF/IOA/meta_theory/Automata.thy
changeset 58957 c9e744ea8a38
parent 58880 0baae4311a9f
child 59807 22bc39064290
     1.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -391,7 +391,6 @@
     1.4  
     1.5  subsection "input_enabledness and par"
     1.6  
     1.7 -
     1.8  (* ugly case distinctions. Heart of proof:
     1.9       1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
    1.10       2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
    1.11 @@ -400,7 +399,7 @@
    1.12        ==> input_enabled (A||B)"
    1.13  apply (unfold input_enabled_def)
    1.14  apply (simp add: Let_def inputs_of_par trans_of_par)
    1.15 -apply (tactic "safe_tac @{theory_context Fun}")
    1.16 +apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})")
    1.17  apply (simp add: inp_is_act)
    1.18  prefer 2
    1.19  apply (simp add: inp_is_act)