Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Multiset.thy
changeset 46238 9ace9e5b79be
parent 46237 99c80c2f841a
child 46394 68f973ffd763 
--- a/src/HOL/Library/Multiset.thy	Tue Jan 17 09:38:30 2012 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Jan 17 10:45:42 2012 +0100
@@ -1078,7 +1078,7 @@
 qed auto
 
 definition
-  "subtract_entries_raw xs ys = foldr (%(k, v). AList_Impl.map_entry k (%v'. v' - v)) ys xs"
+  "subtract_entries_raw xs ys = foldr (%(k, v). AList.map_entry k (%v'. v' - v)) ys xs"
 
 lemma map_of_subtract_entries_raw:
   "distinct (map fst ys) ==> map_of (subtract_entries_raw xs ys) x = (case map_of xs x of None => None | Some v => (case map_of ys x of None => Some v | Some v' => Some (v - v')))"
isabelle