Nominal/Ex/LetRecB.thy
changeset 2950 0911cb7bf696
parent 2922 a27215ab674e
equal deleted inserted replaced
2949:adf22ee09738 2950:0911cb7bf696
     6 
     6 
     7 nominal_datatype let_rec:
     7 nominal_datatype let_rec:
     8  trm =
     8  trm =
     9   Var "name"
     9   Var "name"
    10 | App "trm" "trm"
    10 | App "trm" "trm"
    11 | Lam x::"name" t::"trm"     bind x in t
    11 | Lam x::"name" t::"trm"     binds x in t
    12 | Let_Rec bp::"bp" t::"trm"  bind "bn bp" in bp t
    12 | Let_Rec bp::"bp" t::"trm"  binds "bn bp" in bp t
    13 and bp =
    13 and bp =
    14   Bp "name" "trm"
    14   Bp "name" "trm"
    15 binder
    15 binder
    16   bn::"bp \<Rightarrow> atom list"
    16   bn::"bp \<Rightarrow> atom list"
    17 where
    17 where