more idiomatic style for local declarations in apply scripts
authorhaftmann
Fri, 15 Feb 2019 07:11:09 +0000
changeset 69813 9d94a6c95113
parent 69812 9487788a94c1
child 69814 5929b172c6fe
more idiomatic style for local declarations in apply scripts
src/HOL/UNITY/Comp/Alloc.thy
--- 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