Synchronize Nominal2_Base_Exec with Nominal2_Base, equivariance for Let, avoid overloading approx twice and changes for new isabelle
theory Sigma
imports Nominal2
begin
atom_decl name
nominal_datatype obj =
Var name
| Obj smlst
| Inv obj string
| Upd obj string method
and smlst =
SMNil
| SMCons string method smlst
and method =
Sig n::name o::obj binds n in o
end