diff -r 02b24877be3e -r e6e6a3da81aa Nominal/Ex/Shallow.thy
--- a/Nominal/Ex/Shallow.thy	Wed Dec 22 21:13:32 2010 +0000
+++ b/Nominal/Ex/Shallow.thy	Wed Dec 22 21:13:44 2010 +0000
@@ -15,6 +15,8 @@
 | App1 "trm1" "trm1"
 | Lam1 xs::"name list" t::"trm1" bind xs in t
 
+thm trm1.strong_exhaust
+
 
 text {* binding a finite set of names *}
 
@@ -23,6 +25,7 @@
 | App2 "trm2" "trm2"
 | Lam2 xs::"name fset" t::"trm2" bind (set) xs in t
 
+thm trm2.strong_exhaust
 
 text {* restricting a finite set of names *}
 
@@ -31,6 +34,7 @@
 | App3 "trm3" "trm3"
 | Lam3 xs::"name fset" t::"trm3" bind (res) xs in t
 
+thm trm3.strong_exhaust
 
 end