--- a/Nominal/Ex/Classical.thy	Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/Classical.thy	Wed Dec 22 09:13:25 2010 +0000
@@ -2,7 +2,7 @@
 imports "../Nominal2"
 begin
 
-(* example from my Urban's PhD *)
+(* example from Urban's PhD *)
 
 atom_decl name
 atom_decl coname
@@ -19,12 +19,16 @@
 thm trm.distinct
 thm trm.induct
 thm trm.exhaust
+thm trm.strong_exhaust
+thm trm.strong_exhaust[simplified]
 thm trm.fv_defs
 thm trm.bn_defs
 thm trm.perm_simps
 thm trm.eq_iff
 thm trm.fv_bn_eqvt
 thm trm.size_eqvt
+thm trm.supp
+thm trm.supp[simplified]