Isabelle2018: C parser tests

tools/c-parser/testfiles/list_reverse.thy

@@ -24,7 +24,7 @@ where
 
 lemma list_empty [simp]:
   shows "list xs NULL = (\<lambda>s. xs = [] \<and> \<box> s)"
-  by (cases xs) (auto intro: ext dest!: sep_conj_mapD)
+  by (cases xs) (auto dest!: sep_conj_mapD)
 
 declare sep_conj_com [simp del]
 declare sep_conj_left_com [simp del]

tools/c-parser/testfiles/list_reverse_norm.thy

@@ -79,7 +79,7 @@ lemma list_heapE:
   by (subst list_restrict_dom [symmetric]) (simp add: list_restrict_dom)
 
 lemma list_heap_update_ignore [simp]:
-  "ptr_val x \<notin> set xs \<Longrightarrow> list (h (x \<mapsto> v)) xs p = list h xs p"
+  "ptr_val x \<notin> set xs \<Longrightarrow> list (h (x := Some v)) xs p = list h xs p"
   by (cases x) (auto elim: list_heapE)
 
 declare typ_simps [simp]

tools/c-parser/testfiles/ptr_auxupd.thy

@@ -14,7 +14,7 @@ begin
 
 definition
   "typ_clear_region ptr bits d \<equiv>
-  \<lambda>x. (fst (d x), if x \<in> {ptr..+2 ^ bits} then empty else (snd (d x)))"
+  \<lambda>x. (fst (d x), if x \<in> {ptr..+2 ^ bits} then Map.empty else (snd (d x)))"
 
 declare [[calculate_modifies_proofs = false]]