Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/IOA/TLS.thy
changeset 62390 842917225d56
parent 62195 799a5306e2ed
child 62441 e5e38e1f2dd4 
--- a/src/HOL/HOLCF/IOA/TLS.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -140,7 +140,7 @@
               \<^bold>\<longrightarrow> (Next (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: split_if)
+  apply (simp split add: if_split)
   text \<open>\<open>TL = UU\<close>\<close>
   apply (rule conjI)
   apply (pair ex)
isabelle