--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Shallow.thy	Mon Nov 15 08:17:11 2010 +0000
@@ -0,0 +1,38 @@
+theory Shallow
+imports "../Nominal2" 
+begin
+
+(* 
+  Various shallow binders
+*)
+
+atom_decl name
+
+text {* binding lists of names *}
+
+nominal_datatype trm1 =
+  Var1 "name"
+| App1 "trm1" "trm1"
+| Lam1 xs::"name list" t::"trm1" bind xs in t
+
+
+text {* binding a finite set of names *}
+
+nominal_datatype trm2 =
+  Var2 "name"
+| App2 "trm2" "trm2"
+| Lam2 xs::"name fset" t::"trm2" bind (set) xs in t
+
+
+text {* restricting a finite set of names *}
+
+nominal_datatype trm3 =
+  Var3 "name"
+| App3 "trm3" "trm3"
+| Lam3 xs::"name fset" t::"trm3" bind (res) xs in t
+
+
+end
+
+
+

--- a/Nominal/ROOT.ML	Mon Nov 15 01:10:02 2010 +0000
+++ b/Nominal/ROOT.ML	Mon Nov 15 08:17:11 2010 +0000
@@ -18,6 +18,7 @@
     "Ex/LetFun",
     "Ex/Modules",
     "Ex/SingleLet",
+    "Ex/Shallow",
     "Ex/TypeSchemes",
     "Ex/TypeVarsTest",
     "Ex/Foo1",