Skip to content

Commit

Permalink
camkes: update to Isabelle2023 mapsto syntax
Browse files Browse the repository at this point in the history
Signed-off-by: Gerwin Klein <[email protected]>
  • Loading branch information
lsf37 committed Oct 6, 2023
1 parent 0f99a75 commit 0d984f3
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion camkes/cdl-refine/Eval_CAMKES_CDL.thy
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ lemma Collect_asid_high__eval_helper:
section \<open>Assorted helpers\<close>
lemma fun_upds_to_map_of[THEN eq_reflection]:
"Map.empty = map_of []"
"(map_of xs(k \<mapsto> v)) = map_of ((k, v) # xs)"
"((map_of xs)(k \<mapsto> v)) = map_of ((k, v) # xs)"
by auto

lemma subst_eqn_helper:
Expand Down

0 comments on commit 0d984f3

Please sign in to comment.