added an intro lemma for freshness of products; set up
the simplifier so that it can deal with the compact and
long notation for freshness constraints (FIXME: it should
also be able to deal with the special case of freshness
of atoms)
structure ROOT =
struct
structure Codegen =
struct
fun double_inc a =
IntInf.+ ((IntInf.* ((2 : IntInf.int), a)), (1 : IntInf.int));
end; (*struct Codegen*)
end; (*struct ROOT*)