| changeset 55565 | f663fc1e653b |
| parent 51143 | 0a2371e7ced3 |
| child 58806 | bb5ab5fce93a |
--- a/src/HOL/Library/DAList.thy Tue Feb 18 23:03:49 2014 +0100 +++ b/src/HOL/Library/DAList.thy Tue Feb 18 23:03:50 2014 +0100 @@ -39,7 +39,7 @@ subsection {* Primitive operations *} -lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of .. +lift_definition lookup :: "('key, 'value) alist \<Rightarrow> 'key \<Rightarrow> 'value option" is map_of . lift_definition empty :: "('key, 'value) alist" is "[]" by simp