--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Foo1.thy	Tue Sep 28 05:56:11 2010 -0400
@@ -0,0 +1,49 @@
+theory Foo1
+imports "../Nominal2" 
+begin
+
+(* 
+  Contrived example that has more than one
+  binding function for a datatype
+*)
+
+atom_decl name
+
+nominal_datatype foo: trm =
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"  bind x in t
+| Let1 a::"assg" t::"trm"  bind "bn1 a" in t
+| Let2 a::"assg" t::"trm"  bind "bn2 a" in t
+| Let3 a::"assg" t::"trm"  bind "bn3 a" in t
+and assg =
+  As "name" "name" "trm"
+binder
+  bn1::"assg \<Rightarrow> atom list" and
+  bn2::"assg \<Rightarrow> atom list" and
+  bn3::"assg \<Rightarrow> atom list"
+where
+  "bn1 (As x y t) = [atom x]"
+| "bn2 (As x y t) = [atom y]"
+| "bn3 (As x y t) = [atom x, atom y]"
+
+thm foo.distinct
+thm foo.induct
+thm foo.inducts
+thm foo.exhaust
+thm foo.fv_defs
+thm foo.bn_defs
+thm foo.perm_simps
+thm foo.eq_iff
+thm foo.fv_bn_eqvt
+thm foo.size_eqvt
+thm foo.supports
+thm foo.fsupp
+thm foo.supp
+thm foo.fresh
+
+
+end
+
+
+