--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -0,0 +1,30 @@
+theory TypeVarsTest
+imports "../NewParser" 
+begin
+
+atom_decl name
+declare [[STEPS = 21]]
+
+class s1
+class s2
+
+nominal_datatype ('a, 'b) lam =
+  Var "name"
+| App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
+| Lam x::"name" l::"('a, 'b) lam"  bind x in l
+
+thm lam.distinct
+thm lam.induct
+thm lam.exhaust
+thm lam.fv_defs
+thm lam.bn_defs
+thm lam.perm_simps
+thm lam.eq_iff
+thm lam.fv_bn_eqvt
+thm lam.size_eqvt
+
+
+end
+
+
+