Nominal/Ex/Ex1.thy
changeset 2625 478c5648e73f
parent 2611 3d101f2f817c
child 2950 0911cb7bf696
equal deleted inserted replaced
2624:bfa48c000aa7 2625:478c5648e73f
    38 thm foo_bar.supports
    38 thm foo_bar.supports
    39 thm foo_bar.fsupp
    39 thm foo_bar.fsupp
    40 thm foo_bar.supp
    40 thm foo_bar.supp
    41 
    41 
    42 lemma
    42 lemma
    43   "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"
    43   "supp (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"
    44 apply(simp only: foo_bar.fv_defs)
    44 apply(simp only: foo_bar.supp)
    45 apply(simp only: foo_bar.bn_defs)
    45 apply(simp only: foo_bar.bn_defs)
    46 apply(simp only: supp_at_base)
    46 apply(simp only: supp_at_base)
    47 apply(simp)
    47 apply(simp)
    48 done
    48 done
    49 
    49