--- a/Nominal/Ex/ExPS3.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/ExPS3.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -6,14 +6,11 @@
 
 atom_decl name
 
-ML {* val _ = cheat_equivp := true *}
-ML {* val _ = cheat_alpha_bn_rsp := true *}
-
 nominal_datatype exp =
   Var "name"
 | App "exp" "exp"
-| Lam x::"name" e::"exp" bind_set x in e
-| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
+| Lam x::"name" e::"exp" bind x in e
+| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind (set) x in e2, bind (set) "bp p" in e1
 and pat =
   PVar "name"
 | PUnit
@@ -25,16 +22,16 @@
 | "bp (PUnit) = {}"
 | "bp (PPair p1 p2) = bp p1 \<union> bp p2"
 
-thm exp_pat.fv
-thm exp_pat.eq_iff
-thm exp_pat.bn
-thm exp_pat.perm
+
+thm exp_pat.distinct
 thm exp_pat.induct
-thm exp_pat.distinct
-thm exp_pat.fv
-thm exp_pat.supp(1-2)
-
-
+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
 
 
 end