From 0d984f3fa3c44c1b5c56ee20b6a67bf4ca869221 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 16 Sep 2023 21:33:41 +0200 Subject: [PATCH] camkes: update to Isabelle2023 mapsto syntax Signed-off-by: Gerwin Klein --- camkes/cdl-refine/Eval_CAMKES_CDL.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/camkes/cdl-refine/Eval_CAMKES_CDL.thy b/camkes/cdl-refine/Eval_CAMKES_CDL.thy index a02b4ad5e..1a1347223 100644 --- a/camkes/cdl-refine/Eval_CAMKES_CDL.thy +++ b/camkes/cdl-refine/Eval_CAMKES_CDL.thy @@ -211,7 +211,7 @@ lemma Collect_asid_high__eval_helper: section \Assorted helpers\ lemma fun_upds_to_map_of[THEN eq_reflection]: "Map.empty = map_of []" - "(map_of xs(k \ v)) = map_of ((k, v) # xs)" + "((map_of xs)(k \ v)) = map_of ((k, v) # xs)" by auto lemma subst_eqn_helper: