[isabelle] Subtractive version of map_add


The function map_add in HOL/Map.thy takes two partial 
functions m1 and m2 and returns a partial function with the 
mappings of m1 present in m2.  Its infix notation is 
m1++m2.  Is there a subtractive version of the same 
function?  In other words, something like m1--m2 which 
removes from m2 any mappings present in m1?


Justin S. Davis

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.