changeset 26359 | 6d437bde2f1d |
parent 25131 | 2c8caac48ade |
child 26806 | 40b411ec05aa |
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Thu Mar 20 12:04:54 2008 +0100 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy Thu Mar 20 12:09:20 2008 +0100 @@ -399,7 +399,7 @@ ==> input_enabled (A||B)" apply (unfold input_enabled_def) apply (simp add: Let_def inputs_of_par trans_of_par) -apply (tactic "safe_tac set_cs") +apply (tactic "safe_tac (claset_of @{theory Fun})") apply (simp add: inp_is_act) prefer 2 apply (simp add: inp_is_act)