equal
deleted
inserted
replaced
40 abbreviation |
40 abbreviation |
41 table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *} |
41 table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *} |
42 where "table_of \<equiv> map_of" |
42 where "table_of \<equiv> map_of" |
43 |
43 |
44 translations |
44 translations |
45 (type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option" |
45 (type) "('a, 'b) table" <= (type) "'a \<rightharpoonup> 'b" |
46 (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b" |
|
47 |
46 |
48 (* ### To map *) |
47 (* ### To map *) |
49 lemma map_add_find_left[simp]: |
48 lemma map_add_find_left[simp]: |
50 "n k = None \<Longrightarrow> (m ++ n) k = m k" |
49 "n k = None \<Longrightarrow> (m ++ n) k = m k" |
51 by (simp add: map_add_def) |
50 by (simp add: map_add_def) |