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/Deadlock.thy
changeset 63549 b0d31c7def86
parent 62390 842917225d56 
--- a/src/HOL/HOLCF/IOA/Deadlock.thy	Mon Jul 25 14:02:29 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Deadlock.thy	Mon Jul 25 21:50:04 2016 +0200
@@ -11,8 +11,8 @@
 text \<open>Input actions may always be added to a schedule.\<close>
 
 lemma scheds_input_enabled:
-  "Filter (\<lambda>x. x \<in> act A) $ sch \<in> schedules A \<Longrightarrow> a \<in> inp A \<Longrightarrow> input_enabled A \<Longrightarrow> Finite sch
-    \<Longrightarrow> Filter (\<lambda>x. x \<in> act A) $ sch @@ a \<leadsto> nil \<in> schedules A"
+  "Filter (\<lambda>x. x \<in> act A) \<cdot> sch \<in> schedules A \<Longrightarrow> a \<in> inp A \<Longrightarrow> input_enabled A \<Longrightarrow> Finite sch
+    \<Longrightarrow> Filter (\<lambda>x. x \<in> act A) \<cdot> sch @@ a \<leadsto> nil \<in> schedules A"
   apply (simp add: schedules_def has_schedule_def)
   apply auto
   apply (frule inp_is_act)
@@ -24,7 +24,7 @@
   apply (simp add: filter_act_def)
   defer
   apply (rule_tac [2] Map2Finite [THEN iffD1])
-  apply (rule_tac [2] t = "Map fst $ ex" in subst)
+  apply (rule_tac [2] t = "Map fst \<cdot> ex" in subst)
   prefer 2
   apply assumption
   apply (erule_tac [2] FiniteFilter)
@@ -60,7 +60,7 @@
   assumes "a \<in> local A"
     and "Finite sch"
     and "sch \<in> schedules (A \<parallel> B)"
-    and "Filter (\<lambda>x. x \<in> act A) $ (sch @@ a \<leadsto> nil) \<in> schedules A"
+    and "Filter (\<lambda>x. x \<in> act A) \<cdot> (sch @@ a \<leadsto> nil) \<in> schedules A"
     and "compatible A B"
     and "input_enabled B"
   shows "(sch @@ a \<leadsto> nil) \<in> schedules (A \<parallel> B)"
isabelle