--- a/Nominal/Ex/TypeSchemes.thy	Sat Sep 04 06:10:04 2010 +0800
+++ b/Nominal/Ex/TypeSchemes.thy	Sat Sep 04 06:23:31 2010 +0800
@@ -14,15 +14,39 @@
 and tys =
   All xs::"name fset" ty::"ty" bind (res) xs in ty
 
+thm ty_tys.distinct
+thm ty_tys.induct
+thm ty_tys.exhaust
+thm ty_tys.fv_defs
+thm ty_tys.bn_defs
+thm ty_tys.perm_simps
+thm ty_tys.eq_iff
+thm ty_tys.fv_bn_eqvt
+thm ty_tys.size_eqvt
+thm ty_tys.supports
+thm ty_tys.fsupp
 
 nominal_datatype ty2 =
   Var2 "name"
 | Fun2 "ty2" "ty2"
 
-
 nominal_datatype tys2 =
   All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
 
+thm tys2.distinct
+thm tys2.induct
+thm tys2.exhaust
+thm tys2.fv_defs
+thm tys2.bn_defs
+thm tys2.perm_simps
+thm tys2.eq_iff
+thm tys2.fv_bn_eqvt
+thm tys2.size_eqvt
+thm tys2.supports
+thm tys2.fsupp
+
+
+text {* *}
 
 (*
 ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *}