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+− +−