TFL/mask.sig

Removal of redundant code (unused or already present in Isabelle.
This eliminates HOL compatibility but makes the code smaller and more
readable

signature Mask_sig =
sig
 datatype 'a binding = |-> of ('a * 'a)  (* infix 7 |->; *)

 type mask
 val ERR : mask

end