diff -r fb201e383f1b -r da575186d492 Nominal/Ex/FiniteType.thy
--- a/Nominal/Ex/FiniteType.thy	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-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
\ No newline at end of file