Nominal/Ex/SingleLet.thy
changeset 2634 3ce1089cdbf3
parent 2622 e6e6a3da81aa
child 2950 0911cb7bf696
equal deleted inserted replaced
2633:d1d09177ec89 2634:3ce1089cdbf3
     9 | App "trm" "trm"
     9 | App "trm" "trm"
    10 | Lam x::"name" t::"trm"  bind x in t
    10 | Lam x::"name" t::"trm"  bind x in t
    11 | Let a::"assg" t::"trm"  bind "bn a" in t
    11 | Let a::"assg" t::"trm"  bind "bn a" in t
    12 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
    12 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
    13 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
    13 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
    14 | Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (res) x in t2 
    14 | Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set+) x in t2 
    15 and assg =
    15 and assg =
    16   As "name" x::"name" t::"trm" bind x in t
    16   As "name" x::"name" t::"trm" bind x in t
    17 binder
    17 binder
    18   bn::"assg \<Rightarrow> atom list"
    18   bn::"assg \<Rightarrow> atom list"
    19 where
    19 where