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: