--- a/Nominal/Ex/CoreHaskell.thy	Tue Aug 17 06:50:49 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Tue Aug 17 07:11:45 2010 +0800
@@ -139,6 +139,20 @@
   val thms_f = map (lift_thm qtys @{context}) @{thms bn_defs}
 *}
 
+ML {*
+  val thms_f = map (lift_thm qtys @{context}) @{thms bn_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm qtys @{context}) @{thms fv_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm qtys @{context}) @{thms size_eqvt}
+*}
+
+
+
 
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]

--- a/Nominal/Ex/SingleLet.thy	Tue Aug 17 06:50:49 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Tue Aug 17 07:11:45 2010 +0800
@@ -31,8 +31,13 @@
 thm trm_raw_assg_raw.size(9 - 16)
 thm eq_iff
 thm eq_iff_simps
+thm bn_defs
+thm fv_eqvt
+thm bn_eqvt
+thm size_eqvt
 
-(* bn / eqvt lemmas for fv / fv_bn / bn *)
+
+(* eqvt lemmas for fv / fv_bn / bn *)
 
 ML {*
   val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
@@ -74,8 +79,20 @@
   val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_defs}
 *}
 
-thm perm_defs
-thm perm_simps
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms size_eqvt}
+*}
+
+
+
 
 lemma supp_fv:
   "supp t = fv_trm t"

--- a/Nominal/NewParser.thy	Tue Aug 17 06:50:49 2010 +0800
+++ b/Nominal/NewParser.thy	Tue Aug 17 07:11:45 2010 +0800
@@ -375,15 +375,15 @@
 
   (* proving equivariance lemmas for bns, fvs, size and alpha *)
   val _ = warning "Proving equivariance";
-  val bn_eqvt = 
+  val raw_bn_eqvt = 
     if get_STEPS lthy > 6
     then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4
     else raise TEST lthy4
 
-  (* noting the bn_eqvt lemmas in a temprorary theory *)
-  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), bn_eqvt) lthy4)
+  (* noting the raw_bn_eqvt lemmas in a temprorary theory *)
+  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_bn_eqvt) lthy4)
 
-  val fv_eqvt = 
+  val raw_fv_eqvt = 
     if get_STEPS lthy > 7
     then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) 
       (Local_Theory.restore lthy_tmp)
@@ -397,7 +397,7 @@
       |> map (fn thm => thm RS @{thm sym})
     else raise TEST lthy4
  
-  val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), fv_eqvt) lthy_tmp)
+  val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_fv_eqvt) lthy_tmp)
 
   val (alpha_eqvt, lthy6) =
     if get_STEPS lthy > 9
@@ -539,6 +539,9 @@
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
      ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms)
+     ||>> Local_Theory.note ((@{binding "fv_eqvt"}, []), raw_fv_eqvt) 
+     ||>> Local_Theory.note ((@{binding "bn_eqvt"}, []), raw_bn_eqvt)      
+     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt)      
 
   val _ = 
     if get_STEPS lthy > 20
@@ -636,7 +639,7 @@
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
   val q_dis = map (lift_thm qtys lthy18) alpha_distincts;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
-  val q_eqvt = map (lift_thm qtys lthy19) (bn_eqvt @ fv_eqvt);
+  val q_eqvt = map (lift_thm qtys lthy19) (raw_bn_eqvt @ raw_fv_eqvt);
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = warning "Supports";