author | Christian Urban <urbanc@in.tum.de> |
Tue, 10 Apr 2012 16:02:30 +0100 | |
changeset 3158 | 89f9d7e85e88 |
parent 3109 | d79e936e30ea |
child 3235 | 5ebd327ffb96 |
permissions | -rw-r--r-- |
theory FiniteType imports "../Nominal2" begin typedef ('a::pt, 'b::fs) ffun = "{f::'a => 'b. finite (supp f)}" apply(rule_tac x="\<lambda>_. undefined::'b::fs" in exI) apply(auto) apply(rule_tac S="supp (undefined::'b::fs)" in supports_finite) apply(simp add: supports_def) apply(perm_simp) apply(simp add: fresh_def[symmetric]) apply(simp add: swap_fresh_fresh) apply(simp add: finite_supp) done end