--- a/Nominal/Ex/TypeVarsTest.thy	Sat May 12 21:39:09 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-theory TypeVarsTest
-imports "../Nominal2" 
-begin
-
-(* a nominal datatype with type variables and sorts *)
-
-
-(* the sort constraints need to be attached to the  *)
-(* first occurence of the type variables on the     *)
-(* right-hand side                                  *)
-
-atom_decl name
-
-class s1
-class s2
-
-instance nat :: s1 ..
-instance int :: s2 .. 
-
-nominal_datatype ('a::s1, 'b::s2, 'c::at) lam =
-  Var "name"
-| App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
-| Lam x::"name" l::"('a, 'b, 'c) lam"  binds x in l
-| Foo "'a" "'b"
-| Bar x::"'c" l::"('a, 'b, 'c) lam"  binds x in l   (* Bar binds a polymorphic atom *)
-
-term Foo
-term Bar
-
-thm lam.distinct
-thm lam.induct
-thm lam.exhaust 
-thm lam.strong_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
-
-
-nominal_datatype ('alpha, 'beta, 'gamma) psi =
-  PsiNil
-| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
-
-
-nominal_datatype 'a foo = 
-  Node x::"name" f::"'a foo" binds x in f
-| Leaf "'a"
-
-term "Leaf"
-
-
-
-
-end
-
-
-