1 theory Sigma

     2 imports Nominal2

     3 begin

     4 

     5 atom_decl name

     6 

     7 nominal_datatype obj =

     8   Var name

     9 | Obj smlst

    10 | Inv obj string

    11 | Upd obj string method

    12 and smlst =

    13   SMNil

    14 | SMCons string method smlst

    15 and method =

    16   Sig n::name o::obj binds n in o

    17 

    18 

    19 end

    20