3 begin

     3 begin

     4 

     4 

     5 text {* example 3 or example 5 from Terms.thy *}

     5 text {* example 3 or example 5 from Terms.thy *}

     6 

     6 

     7 atom_decl name

     7 atom_decl name

     8 

    10 

     9 nominal_datatype trm =

    11 nominal_datatype trm =

    10   Var "name"

    12   Var "name"

    11 | App "trm" "trm"

    13 | App "trm" "trm"

    12 | Lam x::"name" t::"trm"  bind  x in t

    14 | Lam x::"name" t::"trm"  bind  x in t