--- /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
+
+
+

--- a/Slides/ROOT1.ML	Thu Sep 23 05:28:40 2010 +0200
+++ b/Slides/ROOT1.ML	Sat Sep 25 02:53:39 2010 +0200
@@ -1,4 +1,4 @@
-show_question_marks := false;
+(* show_question_marks := false; *)
 quick_and_dirty := true;
 
 no_document use_thy "LaTeXsugar";

--- a/Slides/ROOT2.ML	Thu Sep 23 05:28:40 2010 +0200
+++ b/Slides/ROOT2.ML	Sat Sep 25 02:53:39 2010 +0200
@@ -1,6 +1,8 @@
-show_question_marks := false;
+(* show_question_marks := false; *)
+
 quick_and_dirty := true;
 
+
 no_document use_thy "LaTeXsugar";
 
 use_thy "Slides2"
\ No newline at end of file