src/HOLCF/IOA/meta_theory/TLS.thy
changeset 26359 6d437bde2f1d
parent 26339 7825c83c9eff
child 27208 5fe899199f85
--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Mar 20 12:04:54 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Mar 20 12:09:20 2008 +0100
@@ -166,7 +166,7 @@
               .--> (Next (Init (%(s,a,t).Q s))))"
 apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
 
-apply (tactic "clarify_tac set_cs 1")
+apply clarify
 apply (simp split add: split_if)
 (* TL = UU *)
 apply (rule conjI)