TFL/mask.sig
author nipkow
Fri, 07 Feb 1997 14:15:35 +0100
changeset 2597 8b523426e1a4
parent 2112 3902e9af752f
child 3302 404fe31fd8d2
permissions -rw-r--r--
Modified proofs due to added triv_forall_equality.

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

 type mask
 val ERR : mask

end