equal
deleted
inserted
replaced
691 lemma distinct_map_default: |
691 lemma distinct_map_default: |
692 assumes "distinct (map fst xs)" |
692 assumes "distinct (map fst xs)" |
693 shows "distinct (map fst (map_default k v f xs))" |
693 shows "distinct (map fst (map_default k v f xs))" |
694 using assms by (induct xs) (auto simp add: dom_map_default) |
694 using assms by (induct xs) (auto simp add: dom_map_default) |
695 |
695 |
696 hide_const (open) map_entry |
696 hide_const (open) update updates delete restrict clearjunk merge compose map_entry |
697 |
697 |
698 end |
698 end |