adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

camkes: update to Isabelle2023 mapsto syntax 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-09-16 21:33:41 +02:00
parent 0f99a75300
commit 0d984f3fa3
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
camkes/cdl-refine/Eval_CAMKES_CDL.thy
View File

@ -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: