diff -r eb9f5ee249f9 -r bdaa0eb0fc74 src/HOL/HOLCF/IOA/TLS.thy
--- a/src/HOL/HOLCF/IOA/TLS.thy	Sat Jan 16 16:37:45 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Sat Jan 16 23:24:50 2016 +0100
@@ -34,13 +34,10 @@
   where "xt2 P tr = P (fst (snd tr))"
 
 definition ex2seqC :: "('a, 's) pairs \<rightarrow> ('s \<Rightarrow> ('a option, 's) transition Seq)"
-where
-  "ex2seqC = (fix$(LAM h ex. (%s. case ex of
-      nil =>  (s,None,s)\<leadsto>nil
-    | x##xs => (flift1 (%pr.
-                (s,Some (fst pr), snd pr)\<leadsto> (h$xs) (snd pr))
-                $x)
-      )))"
+  where "ex2seqC =
+    (fix $ (LAM h ex. (\<lambda>s. case ex of
+      nil \<Rightarrow> (s, None, s) \<leadsto> nil
+    | x ## xs \<Rightarrow> (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (h $ xs) (snd pr)) $ x))))"
 
 definition ex2seq :: "('a, 's) execution \<Rightarrow> ('a option, 's) transition Seq"
   where "ex2seq ex = (ex2seqC $ (mkfin (snd ex))) (fst ex)"
@@ -56,16 +53,9 @@
 
 
 axiomatization
-where
-
-mkfin_UU:
-  "mkfin UU = nil" and
-
-mkfin_nil:
-  "mkfin nil =nil" and
-
-mkfin_cons:
-  "(mkfin (a\<leadsto>s)) = (a\<leadsto>(mkfin s))"
+where mkfin_UU [simp]: "mkfin UU = nil"
+  and mkfin_nil [simp]: "mkfin nil = nil"
+  and mkfin_cons [simp]: "mkfin (a \<leadsto> s) = a \<leadsto> mkfin s"
 
 
 lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
@@ -75,12 +65,12 @@
 
 subsection \<open>ex2seqC\<close>
 
-lemma ex2seqC_unfold: "ex2seqC  = (LAM ex. (%s. case ex of
-       nil =>  (s,None,s)\<leadsto>nil
-     | x##xs => (flift1 (%pr.
-                 (s,Some (fst pr), snd pr)\<leadsto> (ex2seqC$xs) (snd pr))
-                 $x)
-       ))"
+lemma ex2seqC_unfold:
+  "ex2seqC =
+    (LAM ex. (\<lambda>s. case ex of
+      nil \<Rightarrow> (s, None, s) \<leadsto> nil
+    | x ## xs \<Rightarrow>
+        (flift1 (\<lambda>pr. (s, Some (fst pr), snd pr) \<leadsto> (ex2seqC $ xs) (snd pr)) $ x)))"
   apply (rule trans)
   apply (rule fix_eq4)
   apply (rule ex2seqC_def)
@@ -88,43 +78,38 @@
   apply (simp add: flift1_def)
   done
 
-lemma ex2seqC_UU: "(ex2seqC $UU) s=UU"
+lemma ex2seqC_UU [simp]: "(ex2seqC $ UU) s = UU"
   apply (subst ex2seqC_unfold)
   apply simp
   done
 
-lemma ex2seqC_nil: "(ex2seqC $nil) s = (s,None,s)\<leadsto>nil"
+lemma ex2seqC_nil [simp]: "(ex2seqC $ nil) s = (s, None, s) \<leadsto> nil"
   apply (subst ex2seqC_unfold)
   apply simp
   done
 
-lemma ex2seqC_cons: "(ex2seqC $((a,t)\<leadsto>xs)) s = (s,Some a,t)\<leadsto> ((ex2seqC$xs) t)"
+lemma ex2seqC_cons [simp]: "(ex2seqC $ ((a, t) \<leadsto> xs)) s = (s, Some a,t ) \<leadsto> (ex2seqC $ xs) t"
   apply (rule trans)
   apply (subst ex2seqC_unfold)
   apply (simp add: Consq_def flift1_def)
   apply (simp add: Consq_def flift1_def)
   done
 
-declare ex2seqC_UU [simp] ex2seqC_nil [simp] ex2seqC_cons [simp]
 
-
-
-declare mkfin_UU [simp] mkfin_nil [simp] mkfin_cons [simp]
-
-lemma ex2seq_UU: "ex2seq (s, UU) = (s,None,s)\<leadsto>nil"
+lemma ex2seq_UU: "ex2seq (s, UU) = (s, None, s) \<leadsto> nil"
   by (simp add: ex2seq_def)
 
-lemma ex2seq_nil: "ex2seq (s, nil) = (s,None,s)\<leadsto>nil"
+lemma ex2seq_nil: "ex2seq (s, nil) = (s, None, s) \<leadsto> nil"
   by (simp add: ex2seq_def)
 
-lemma ex2seq_cons: "ex2seq (s, (a,t)\<leadsto>ex) = (s,Some a,t) \<leadsto> ex2seq (t, ex)"
+lemma ex2seq_cons: "ex2seq (s, (a, t) \<leadsto> ex) = (s, Some a, t) \<leadsto> ex2seq (t, ex)"
   by (simp add: ex2seq_def)
 
 declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del]
 declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp]
 
 
-lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
+lemma ex2seq_nUUnnil: "ex2seq exec \<noteq> UU \<and> ex2seq exec \<noteq> nil"
   apply (tactic \<open>pair_tac @{context} "exec" 1\<close>)
   apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
@@ -137,21 +122,20 @@
    after the translation via ex2seq !! *)
 
 lemma TL_TLS:
-  "[| ! s a t. (P s) & s \<midarrow>a\<midarrow>A\<rightarrow> t --> (Q t) |]
-    ==> ex \<TTurnstile> (Init (%(s,a,t). P s) \<^bold>\<and> Init (%(s,a,t). s \<midarrow>a\<midarrow>A\<rightarrow> t)
-              \<^bold>\<longrightarrow> (Next (Init (%(s,a,t).Q s))))"
+  "\<forall>s a t. (P s) \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> (Q t)
+    \<Longrightarrow> ex \<TTurnstile> (Init (\<lambda>(s, a, t). P s) \<^bold>\<and> Init (\<lambda>(s, a, t). s \<midarrow>a\<midarrow>A\<rightarrow> t)
+              \<^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)
-  (* TL = UU *)
+  text \<open>\<open>TL = UU\<close>\<close>
   apply (rule conjI)
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
   apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-  (* TL = nil *)
+  text \<open>\<open>TL = nil\<close>\<close>
   apply (rule conjI)
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (tactic \<open>Seq_case_tac @{context} "x2" 1\<close>)
@@ -163,9 +147,8 @@
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
   apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-  (* TL =cons *)
+  text \<open>\<open>TL = cons\<close>\<close>
   apply (simp add: unlift_def)
-
   apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
   apply (tactic \<open>pair_tac @{context} "a" 1\<close>)