diff -r 594f3401605f -r 6bab47906dbe Nominal/Ex/Datatypes.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Datatypes.thy	Sat Sep 25 02:53:39 2010 +0200
@@ -0,0 +1,68 @@
+theory Datatypes
+imports "../Nominal2" 
+begin
+
+(* 
+  plain nominal_datatype definition without an 
+  atom_decl - example by John Matthews
+*)
+
+nominal_datatype 'a Maybe = 
+  Nothing 
+| Just 'a
+
+
+thm Maybe.distinct
+thm Maybe.induct
+thm Maybe.exhaust
+thm Maybe.fv_defs
+thm Maybe.bn_defs
+thm Maybe.perm_simps
+thm Maybe.eq_iff
+thm Maybe.fv_bn_eqvt
+thm Maybe.size_eqvt
+thm Maybe.supp
+
+(*
+  using a datatype inside a nominal_datatype
+*)
+
+atom_decl name
+
+datatype foo = Foo | Bar
+
+
+instantiation foo :: pure
+begin
+
+definition
+  "p \<bullet> (f::foo) = f"
+
+instance
+apply(default)
+apply(simp_all add:  permute_foo_def)
+done
+
+end
+
+
+nominal_datatype baz =
+  Baz x::name t::foo bind x in t
+
+
+thm baz.distinct
+thm baz.induct
+thm baz.exhaust
+thm baz.fv_defs
+thm baz.bn_defs
+thm baz.perm_simps
+thm baz.eq_iff
+thm baz.fv_bn_eqvt
+thm baz.size_eqvt
+thm baz.supp
+  
+
+end
+
+
+