Nominal/Ex/SingleLet.thy
changeset 2106 409ecb7284dd
parent 2105 e25b0fff0dd2
child 2107 5686d83db1f9
equal deleted inserted replaced
2105:e25b0fff0dd2 2106:409ecb7284dd
    13   As "name" "trm"
    13   As "name" "trm"
    14 binder
    14 binder
    15   bn::"assg \<Rightarrow> atom set"
    15   bn::"assg \<Rightarrow> atom set"
    16 where
    16 where
    17   "bn (As x t) = {atom x}"
    17   "bn (As x t) = {atom x}"
       
    18 
    18 
    19 
    19 thm trm_assg.fv
    20 thm trm_assg.fv
    20 thm trm_assg.supp
    21 thm trm_assg.supp
    21 thm trm_assg.eq_iff
    22 thm trm_assg.eq_iff
    22 thm trm_assg.bn
    23 thm trm_assg.bn