# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1289809031 0
# Node ID 1c77e15c4259d6bfebfc9d0aafef41160a369746
# Parent  94750b31a97d468965e2f3a69eb5709013fc12db
added a test for the various shallow binders

diff -r 94750b31a97d -r 1c77e15c4259 Nominal/Ex/Shallow.thy
--- /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
+
+
+
diff -r 94750b31a97d -r 1c77e15c4259 Nominal/ROOT.ML
--- 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",