--- a/Nominal/Ex/Datatypes.thy	Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/Datatypes.thy	Wed Dec 22 09:13:25 2010 +0000
@@ -17,6 +17,7 @@
 thm Maybe.distinct
 thm Maybe.induct
 thm Maybe.exhaust
+thm Maybe.strong_exhaust
 thm Maybe.fv_defs
 thm Maybe.bn_defs
 thm Maybe.perm_simps
@@ -27,6 +28,9 @@
 
 (*
   using a datatype inside a nominal_datatype
+
+  the datatype needs to be shown to be an instance
+  of the pure class (this is usually trivial)
 *)
 
 atom_decl name
@@ -55,6 +59,7 @@
 thm baz.distinct
 thm baz.induct
 thm baz.exhaust
+thm baz.strong_exhaust
 thm baz.fv_defs
 thm baz.bn_defs
 thm baz.perm_simps