--- a/Nominal/Test.thy	Sat Feb 27 11:54:59 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 01 07:46:50 2010 +0100
@@ -63,6 +63,7 @@
 thm f0_raw.simps
 
 text {* example type schemes *}
+
 datatype t = 
   Var "name" 
 | Fun "t" "t"
@@ -197,8 +198,20 @@
   "bv9 (Var9 x) = {}"
 | "bv9 (Lam9 x b) = {atom x}"
 
-(* example form Leroy 96 about modules *)
+(* example from my PHD *)
+
+atom_decl coname
 
+nominal_datatype phd =
+   Ax name coname
+|  Cut n::name t1::phd c::coname t2::phd               bind n in t1, bind c in t2
+|  AndR c1::coname t1::phd c2::coname t2::phd coname   bind c1 in t1, bind c2 in t2
+|  AndL1 n::name t::phd name                           bind n in t
+|  AndL2 n::name t::phd name                           bind n in t
+|  ImpL c::coname t1::phd n::name t2::phd name         bind c in t1, bind n in t2
+|  ImpR c::coname n::name t::phd coname                bind n in 1, bind c in t
+
+(* example form Leroy 96 about modules; OTT *)
 
 nominal_datatype mexp =
   Acc path