--- a/Nominal/Ex/LetFun.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/Ex/LetFun.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -4,8 +4,11 @@
 
 atom_decl name
 
-(* x is bound in both e1 and e2
-   names in p are bound only in e1 *)
+(* x is bound in both e1 and e2;
+   bp-names in p are bound only in e1 
+*)
+
+declare [[STEPS = 100]]
 
 nominal_datatype exp =
   Var name
@@ -22,4 +25,19 @@
 | "bp (PUnit) = []"
 | "bp (PPair p1 p2) = bp p1 @ bp p2"
 
+thm exp_pat.distinct
+thm exp_pat.induct
+thm exp_pat.inducts
+thm exp_pat.exhaust
+thm exp_pat.fv_defs
+thm exp_pat.bn_defs
+thm exp_pat.perm_simps
+thm exp_pat.eq_iff
+thm exp_pat.fv_bn_eqvt
+thm exp_pat.size_eqvt
+thm exp_pat.supports
+thm exp_pat.fsupp
+thm exp_pat.supp
+
+
 end
\ No newline at end of file