diff -r d29a8a6f3138 -r 75a95431cd8b Nominal/Ex/Datatypes.thy
--- a/Nominal/Ex/Datatypes.thy	Thu Apr 28 11:51:01 2011 +0800
+++ b/Nominal/Ex/Datatypes.thy	Tue May 03 13:09:08 2011 +0100
@@ -67,7 +67,29 @@
 thm baz.fv_bn_eqvt
 thm baz.size_eqvt
 thm baz.supp
+
+(*
+  a nominal datatype with a set argument of
+  pure type
+*)
   
+nominal_datatype set_ty = 
+  Set_ty "nat set"
+| Fun "nat \<Rightarrow> nat"
+| Var "name"
+| Lam x::"name" t::"set_ty" bind x in t
+
+thm set_ty.distinct
+thm set_ty.induct
+thm set_ty.exhaust
+thm set_ty.strong_exhaust
+thm set_ty.fv_defs
+thm set_ty.bn_defs
+thm set_ty.perm_simps
+thm set_ty.eq_iff
+thm set_ty.fv_bn_eqvt
+thm set_ty.size_eqvt
+thm set_ty.supp
 
 end