src/HOL/HOLCF/IOA/TLS.thy

--- a/src/HOL/HOLCF/IOA/TLS.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -140,7 +140,7 @@
               \<^bold>\<longrightarrow> (\<circle>(Init (\<lambda>(s, a, t). Q s))))"
   apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
   apply clarify
-  apply (simp split add: if_split)
+  apply (simp split: if_split)
   text \<open>\<open>TL = UU\<close>\<close>
   apply (rule conjI)
   apply (pair ex)