author | haftmann |
Fri, 15 Feb 2019 07:11:09 +0000 | |
changeset 69813 | 9d94a6c95113 |
parent 69812 | 9487788a94c1 |
child 69814 | 5929b172c6fe |
--- a/src/HOL/UNITY/Comp/Alloc.thy Fri Feb 15 17:10:09 2019 +0100 +++ b/src/HOL/UNITY/Comp/Alloc.thy Fri Feb 15 07:11:09 2019 +0000 @@ -962,7 +962,7 @@ (INT h. {s. h \<le> (giv o sub i o client) s & h pfixGe (ask o sub i o client) s} LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})" - using image_cong_simp [cong del] + supply image_cong_simp [cong del] apply rename_client_map apply (simp add: Client_Progress [simplified o_def]) done